Alex Ozdemir on where Theorem Provers and ZK meet

Alex Ozdemir is an assistant professor at Georgia Tech working at the intersection of formal verification, theorem proving, and zero-knowledge proofs. His project ZK Pi is a ZK SNARK for proofs expressed in Lean, allowing a prover to convince a verifier that a Lean theorem is true without revealing the proof itself. His compiler infrastructure project Cersei has evolved to support more expressive and efficient ZK proof systems and sits beneath ZK Pi in the implementation stack.

ZKVMs make circuits an implementation detail rather than a direct interface for application developers, but they do not make circuits obsolete because VMs are themselves implemented using circuits. ZKVMs impose significant performance costs because they require a generic proof about an instruction architecture like RISC-V, which was designed for processor efficiency rather than ZK proof efficiency. Google released a library called Longfellow for anonymous credentials that uses bespoke circuits rather than a ZKVM, illustrating that the performance tradeoff still drives teams toward custom circuits in production settings.

Among ZK DSLs, Circom remains the most widely used by number of projects though its market share as a percentage is declining because other languages are adding new projects faster. Noir's compiler is now the largest of the ZK DSL compilers by lines of code. Clean is a new ZKDSL from ZK Security focused on verification-first design, co-designing the DSL with a verification toolchain. Cairo evolved from a Python-like language to a Rust-like language and sits on top of the Cairo VM as its instruction set. A recurring pattern is that each new proof system requires a new language or gadget library built on top of it, as seen with Libsnark, Bellman, and Halo2.

A newer direction in ZK DSLs involves circuits that can flip coins, modeling interactive proof systems rather than purely deterministic circuits. Random coins correspond to verifier challenges, and a generic SNARK can turn an interactive proof system defined by a randomized circuit into a SNARK for the same property. Lookup arguments can be implemented using random coin challenges, meaning random coins subsume what lookups can do. Cersei is the only compiler that automatically optimizes how randomness is used inside a circuit rather than merely permitting it. Cersei knows four different memory arguments and selects the optimal one based on memory size and number of accesses, can replace matrix multiplication with randomized tests, and can reduce the number of challenges in a program from as many as a thousand down to ten by identifying components that can share challenges. Ozdemir notes that the limits of what randomness optimizations are sound are not yet fully known, and this work has been ongoing for about two years.

Formal verification of Cersei has been a goal from the beginning. The team chose to verify the type-mapping pass first because those passes are often incorrect and because the underlying SMT solver tooling needed to be built regardless of approach. SMT solvers needed for ZK compiler verification did not exist when the project began around 2021 or 2022, so foundational infrastructure had to be built first, and bugs were found in the type-mapping pass before verification of that pass was completed. Ozdemir spent several years developing proof search procedures for finite fields inside the SMT solver CVC5, describing it as the first effective SMT solver for reasoning about finite fields in the ZK domain. Finite fields are central to nearly everything in cryptography including elliptic curves.

ZK Pi is implemented on top of Cersei, which is built on top of the Mirage Plus proof system. Mirage Plus carries a formal security theorem stating that if a circuit encodes an interactive proof that is sound and complete for some language, the resulting construction is a ZK SNARK, and it is the first system to formally state a security theorem capturing what it means to have a SNARK for a randomized circuit. Because Mirage Plus is based on Groth16 it requires a per-circuit trusted setup, making it suitable for academic work but less so for production systems. Lean proofs are large, and ZK Pi both adds zero knowledge and compresses them, with ZK proofs coming in around 200 bytes. The core technical challenge is proving in zero knowledge that a dependent type program is well typed using the calculus of inductive constructions, which is how Lean reduces theorem truth to well-typedness via the Curry-Howard correspondence.

Ozdemir draws a sharp distinction between whether a theorem is correctly specified and whether a proof of that theorem is valid. An adversary abusing formal verification would write the wrong theorem or include a false axiom as a starting premise, making the theorem trivially provable but meaningless. In ZK Pi the Lean proof is hidden but the theorem and axioms are not, so the zero knowledge aspect is entirely orthogonal to whether the theorem itself is correct. He describes detecting or preventing incorrect theorem specification as an open research question not solved by the ZK approach.