Mathias and Giorgio join Anna Rose and fellow zkSecurity teammates Nico and Kobi on the Zero Knowledge podcast to talk about Clean, zkGolf, and what happens when AI agents compete to build better circuits with proofs of correctness.
Cryptographic software is error-prone and failures are catastrophic, therefore formal verification is a powerful and increasingly practical tool for greatly improving the assurances of our cryptographic software. But who verifies the formal verification? Formal verification itself is software too, what is proved, under which assumptions and its relation to the real-world implementation lie beyond the scope of the machine-checked proof. In this post, we want to give some insights into our three-week audit of the Ironwood formalization and some of the common pitfalls that formal verification more broadly can encounter.
In Session 11 of "Proof is in the Pudding," we look at what it takes to prove model inference. We cover transformer computation, sumcheck, GKR, lookup arguments, quantization, and KV caching, then discuss scaling and possible uses for verifiable ML.
In this final post of the series, we extend univariate KZG commitments to multilinear polynomials through Mercury. Building on Gemini, we fold half of the variables at once, use polynomial division to bind this large fold to the original commitment and reduce the remaining multilinear evaluations to a batched inner product check. We then walk through the end-to-end opening protocol. We conclude by examining its proof size, prover cost and verifier cost.
In this blog post, we extend univariate KZG commitments to multilinear polynomials through Gemini. We introduce recursive partial evaluations, derive the split-and-fold identity and express each fold as a univariate identity that can be checked using KZG openings. We then walk through the end-to-end opening protocol. We conclude by examining its proof size, prover cost, and verifier cost.
In this blog post, we extend univariate KZG commitments to multilinear polynomials through Zeromorph. We introduce the univariatization map, encode the multilinear quotient identity as a univariate identity, and explain why the quotient encodings require degree checks. We then show how Zeromorph batches these checks into a single degree-bounded KZG opening and walk through its end-to-end opening protocol. We conclude by examining its proof size, prover cost, and verifier cost.
We think that Clean is the future of circuit development, so we created a programmer-first introduction to show circuit developers who have never used formal verification how they can build circuits faster, safer and better.
This blog post looks at Fiat-Shamir from a practical security perspective: it explains why something that seems simple in theory can become surprisingly easy to get wrong. By using vulnerabilities found in real-world projects, we give developers and reviewers a better way to think about Fiat-Shamir when designing, implementing, and auditing proof systems.
An exploration of how an AI tried to work around a security feature to handle a theorem that was hard to prove.
The economics of security have changed. AI has made finding and exploiting bugs cheaper, including in cryptographic and zero-knowledge code, while validation and remediation remain slow. Here is our view of what happened, what comes next, and how teams should change the way they secure their stack to defend against AI-assisted attackers.
Many of us are using AI to generate code. Vibe coding cryptography is especially sensitive - you have to uphold strict mathematical correctness. This can lead to wrong security guarantees and soundness bugs. We will discuss what are some patterns to do it well.
zkVMs are moving to the center of Ethereum's roadmap, which means a bug in a zkVM is turning into a bug in Ethereum itself. We built zkvmBlast, a zkVM-agnostic differential fuzzer that runs the same program across SP1, RISC0, OpenVM, Pico, Zisk, and Airbender against a reference simulator and flags any disagreement. It hunts for both soundness and completeness bugs, with a deliberate focus on completeness, an under-explored class that can turn a single valid block into a liveness failure. We share the first batch of findings.
