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. It's not scary, we promise.
You can find this on our new official Clean site!
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.
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.
We're diving into our new project called **clean**, aimed at creating an embedded DSL and formal verification framework for Zero Knowledge (ZK) circuits using Lean4. Imagine being able to not only define ZK circuits but also formally prove their correctness. Sounds like a game-changer, right? We'll walk you through our process of building a robust library of reusable, verified circuit gadgets, focusing on the importance of soundness and completeness. Plus, you'll get a peek at some cool examples like 8-bit addition and how we're tackling ZKVM design with techniques borrowed from Fibonacci sequences. It's exciting stuff, and if you're curious about how we're paving the way for bug-free ZK circuits, this is a read you won't want to miss!
Kevin Buzzard, a mathematician with a cautious view on human-checked proofs, found solace in interactive theorem provers, which verify mathematical proofs much like type-checking in programming. We explore how these tools, which are gaining traction in fields like applied cryptography, ensure rigorous and reliable proofs. With Lean as our focus, you'll discover how to dive into this fascinating world, see a proof in action, and learn how this technology is revolutionizing areas like zero-knowledge virtual machines. Curious about building rock-solid, machine-verified proofs? Check out our beginner-friendly guide!
We walk through a Lean 4 proof of correctness for a Clean model of circomlib's optimized Poseidon hash circuit at arity 1. The theorem says the modeled constraints are sound and complete with respect to the optimized Poseidon spec. After weeks of work, the only remaining `sorry` was a primality proof for the BN254 scalar field: a 254-bit number that no proof assistant can decide by trial division. Closing it requires a Pratt certificate, a recursive proof structure based on a theorem Lucas published in 1876.
A step-by-step build of CGGMP, an n-of-n threshold ECDSA scheme where parties jointly produce a signature without ever reconstructing the private key. We start from the multiplicative-to-additive (MtA) protocol and a semi-honest version of the signing protocol, then harden it into a maliciously secure one by layering in zero-knowledge proofs at each step. Along the way we cover the auxiliary Ring-Pedersen and Paillier parameters and the proofs that make them safe to use.
We are releasing zk-skills, a set of open-source security skills for AI coding agents, starting with circom-auditor: a first line of defense against vulnerabilities in Circom circuits, compatible with both Claude Code and Codex. On the zkbugs benchmark it detects up to 66 of 70 known bugs when pointed at the vulnerable circuits, and up to 40 of 56 when let loose on the full original codebases, far ahead of existing Circom security tools.
Zero-knowledge proofs have come a long way in 40 years, thanks to groundbreaking work from many brilliant minds. We're taking you on a tour of the key milestones in this fascinating journey, from the foundational concepts in 1985 by Goldwasser, Micali, and Rackoff, to modern applications and innovations like STARKs and zkVMs. You'll get a taste of major papers and projects that have pushed these proofs from theoretical curiosity to practical and scalable solutions. Dive into the history, understand the evolution, and see how these cryptographic marvels continue to shape the future of secure computation!