ZK/SEC Quarterly

Back to all posts

Comparison of formal verification frameworks for arithmetic circuits

Yoichi Hirai November 19, 2025 18 min read

Comparison of formal verification frameworks for arithmetic circuits

Prelude: Proof Market

In 2014 I was running a website called Proof Market where you could put a bounty in Bitcoin on mathematical statements to be proven and when you prove them in Rocq you could receive the Bitcoin. I want to build a non-custodian version of Proof Market. For that purpose, zkVM can be very useful. I prefer that the proof-checking zkVM be formally verified. I am verifying arithmetic circuits because I want a market for theorem proving people and theorem proving AIs so that I can easily offload the verification of arithmetic circuits!

What

When you encode a problem (something to prove for Proof Market, or in general some verification to pass) as a puzzle of solving polynomial equations, cryptographers give you succinct ways to show that there's a solution to the puzzle (succinct arguments).

The receiver of a succinct argument will be able to check, given some cryptographic assumptions, with a very high probability, that there is a solution to the polynomial puzzle. Then the receiver will also want to make sure that the solution of the polynomial puzzle corresponds to a solution of the original problem (soundness). Also it's often critical for the sender of a succinct argument that any solution of the original problem can be encoded as a polynomial puzzle solution (completeness).

When people write polynomial puzzles (arithmetic circuits), they often have mathematical proofs of soundness and completeness in their mind. Mathematical proofs can be transferred with whiteboards and discussions, but (i) it takes a lot of effort from both sides, the sender and the receiver of the mathematical ideas, and (ii) everybody gets bored after checking five cases out of 40. They get used to some repetitive patterns and lose attention (though I have a hypothesis that it's possible to distinguish theoretical computer scientists from mathematicians by showing them proofs involving 40 cases). Sometimes people miss a slight mistake in the sixth case out of 40 and that matters because an attacker can study that case to find a hole in the implementation.

There are computer languages for writing and checking mathematical proofs, and they can be used to reason about hardware and software systems too. In case of arithmetic circuits the software is written with polynomials, so we are back to math. People have used these to check soundness and completeness of arithmetic circuits. Let me compare these.

Note

For cryptographers: I'm ignoring the argument of knowledge in this blog post. None of the projects mentioned below seems to state that the prover has a polynomial-time access to the solutions. It's all about existence of solutions.

Disclaimer: I'm biased

I'm developing Clean, a framework for proving correctness of arithmetic circuits in a somewhat modular way. Clean is written in Lean Language (TM of Lean FRO).

I used Rocq for years in my jobs. For an early-era formal verification of smart contracts, I used Isabelle. I used ACL2 from time to time for small projects. I've talked with people developing these tools, but I don't belong in the inner circle of any tool developments.

Template

Summary Comparison

Here's the summary of results. Note that the Level 0 examples are only about the publicly available examples. The projects have different goals. Two of them, acl2-jolt and sp1-lean, aim at tricky aspects of existing zkVM implementations. The others aim to be general frameworks. Some try to import circuits from other languages and verify them. Others aim to be frontends. All of the projects contain components that can be reused.

Framework Language Example Level Reproducible Claude Code: IsZero Claude Code: Weighted-Sum
ACL2 (r1cs) ACL2 Level 2? Yes (3 hours) Yes Yes
ACL2 (PFCS) ACL2 Level 1 Yes (no extra time) Yes (one-shot) Yes (verbose)
acl2-jolt ACL2 Level 2 Partial (Ubuntu only) N/A N/A
Garden Rocq Level 2 Yes (20 min) Eventually yes Yes (with intervention)
zk-lean Lean Level 1 Yes (<10 min) No N/A
sp1-lean Lean Level 2 Partial N/A N/A
Clean Lean Level 2 N/A (author) N/A (exists) No

Circuit visualization Image generated by ChatGPT

ACL2 (r1cs) like in the ACL2 book

People used ACL2 for verifying arithmetic circuits. An example is a page in the ACL2 book. The framework lives in the ACL2 book and some applications seem to be proprietary.

R1CS is a popular format of polynomial equations. It seems that the ACL2 (r1cs) library can deal with other kinds of polynomial equations too.

What I like about ACL2 (r1cs) like in ACL2 book

The formalization of the arithmetic circuits is straightforward and easy to follow. There's a list of equations with the left-hand side and the right-hand side spelled out.

(define make-rel-iszero ()
  :returns (def definitionp)
  (make-definition
   :name 'rel-iszero
   :para '(x out)
   :body (list
          ;; Constraint 1: x * x_inv = 1 - out
          (make-constraint-equal
           :left (expression-mul
                  (expression-var 'x)
                  (expression-var 'x-inv))
           :right (expression-sub (expression-const 1)
                                  (expression-var 'out)))
          ;; Constraint 2: out * x = 0
          (make-constraint-equal
           :left (expression-mul
                  (expression-var 'out)
                  (expression-var 'x))
           :right (expression-const 0)))))

ACL2 doesn't require writing tactics in the normal usage. You can give hints to the prover, and it's just about naming the relevant lemmas. This might be easier for humans as well as for LLMs.

My remaining wishes about ACL2 (r1cs) like in ACL2 book

Installation of ACL2 took some trial and error, though this is my third time doing this. I tried to use the particular gcl version mentioned in the installation guide, and the ./configure script didn't work, etc. Some of the online documentation pages returned 403 errors. It's a real hurdle when compared with Lean installation (installing a VSCode plugin and pressing 'ok' a couple of times).

Me vs Claude Code

Claude Code is better than me at dealing with ACL2 (r1cs) like in ACL2 book. I believe that stating and proving correctness theorems happened 100x faster with Claude Code than just me doing it.

ACL2 (PFCS) like in the ACL2 book

What I like about ACL2 (PFCS) like in the ACL2 book

PFCS is a reasonable way to package arithmetic circuits.

My remaining wishes about ACL2 (PFCS) like in the ACL2 book

This framework deserves more attention. It's suffering from the lack of publicly available advanced examples.

There are data types that can be encoded as vectors of field elements, and allowing those as parameters might be an interesting direction.

Me vs Claude Code

It's unclear whether I'm better or Claude Code is in dealing with ACL2 (PFCS). I had a better grasp when Claude Code was about to give up but I insisted on continuing.

ACL2 like in acl2-jolt

Another project using ACL2 is acl2-jolt available on GitHub.

What I like about ACL2 like in acl2-jolt

The project was verifying a real implementation. A part of the codebase is well-documented. The codebase is very uniform and the proven statements are short and easy to read.

My remaining wishes about ACL2 like in acl2-jolt

The verification stops at each instruction. The notion of the program execution has not been formalized. Most users care about execution of programs, so it's important that circuits represent program executions.

There are some confusing aspects in the codebase. Some subtables are made with 257x257 dimension with (create-tuple-indices (expt 2 8) (expt 2 8)). Other subtables are made with 256x256 dimension with (create-tuple-indices (1- (expt 2 8)) (1- (expt 2 8))). I'm mostly sure it doesn't matter, but something similar might matter.

Me vs Claude Code

Claude Code is better than me at dealing with acl2-jolt. I was replacing 257x257 table with a 256x256 table and Claude Code was fixing proofs before I understood why they were broken.

Garden

Garden is a framework for verifying arithmetic circuits written in Rocq.

What I like about Garden

It verifies circuits written in popular DSLs.

My remaining wishes about Garden

Only solvable problems:

The IsZero circuit looks like this

Definition constrain {p} `{Prime p} (arg_fun_0 : IsZero.t) (arg_fun_1 : Felt.t) : M.t unit :=
  let var_out : Felt.t := arg_fun_0.(IsZero.out) in
  let var_inv : Felt.t := arg_fun_0.(IsZero.inv) in
  let var_felt_const_1 : Felt.t := UnOp.from 1 in
  let var_felt_const_0 : Felt.t := UnOp.from 0 in
  (* Constraint 1: out = 1 - x * inv *)
  let var_prod : Felt.t := BinOp.mul arg_fun_1 var_inv in
  let var_out_expr : Felt.t := BinOp.sub var_felt_const_1 var_prod in
  let* _ : unit := M.AssertEqual var_out var_out_expr in
  (* Constraint 2: x * out = 0 *)
  let var_prod2 : Felt.t := BinOp.mul arg_fun_1 var_out in
  let* _ : unit := M.AssertEqual var_prod2 var_felt_const_0 in
  M.Pure tt.

Me vs Claude Code

I'm better than Claude Code at dealing with Garden code.

zk-lean

zk-lean is a framework for verifying arithmetic circuits written in Lean.

What I like about zk-lean

It's too early to tell. The codebase is a combination of a few, very elementary examples and some sophisticated machinery. I will need to see the sophisticated machinery at work before I can say something.

My remaining wishes about zk-lean

I guess more interesting examples are coming. Jolt repository has a feature of exporting some Lean definitions for zk-lean, so there might be some efforts on top of this.

Me vs Claude Code

For me vs Claude Code, about dealing with zk-lean code, it's a tie. Both failed to understand how to reason about the syntax. The point I gave up was when I saw the definition of FreeM.bind is protected. I guessed I wasn't supposed to unfold the definition (unfolding is the act of replacing FreeM.bind with its definition), but then what else?

sp1-lean

Succinct announced formal verification of Sp1 Hypercube. This is a notable achievement.

What I like about sp1-lean

The announcement is very transparent about what the team did and what they didn't do. I especially appreciate the "Assumptions and Caveats" section. The level of transparency is an example to follow.

The effort aimed at verifying all relevant instructions.

The definitions and the statements are easy to follow if you're familiar with RISC-V zkVMs (ways of encoding VM executions into arithmetic circuits).

I feel considerable theorem-proving kung-fu applied in a targeted manner to finish the work. The repo contains cool Lean techniques (use of advanced attributes and skillfully adjusted invocations of automatic tactics) that keep the size of proof scripts to, say, less than 1/5 of what I expect for a naive approach.

My remaining wishes about sp1-lean

The announcement does not specify the git commit of the proof artifacts. The most recent commit at the time of announcement doesn't contain completed proof of LB correctness. A previous commit contains a theorem about LB instruction.

Completeness is missing. For instance correct_add says "if constraints hold, something something". I could not find another theorem saying "if something something, constraints can be satisfied".

There are some tricky points about the definitions. The mitigation would involve some design changes in the constraint development framework:

The proofs look fragile to changes in the number of constraints etc. Perhaps coding agents are able to update this kind of things.

Clean

Clean is a framework for proving correctness of arithmetic circuits in a modular way, written in Lean.

What I like about Clean

The whole development is in Lean, so nothing is lost in translation.

Clean offers ways to verify sub-circuits in a composable way.

There's some conceptual simplicity about looking at everything as a predicate on the infinite tape of field variables.

The circuit syntax is passable as a front-end language (in my opinion). Here's a IsZeroField.lean in Clean project (written before this experiment):

def main (x : Var field F) : Circuit F (Var field F) := do
  -- When x ≠ 0, we need x_inv such that x * x_inv = 1
  -- When x = 0, x_inv can be anything (we use 0)
  let xInv ← witness fun env =>
    if x.eval env = 0 then 0 else (x.eval env : F)⁻¹

  let isZero <== 1 - x*xInv -- If x is zero, isZero is one
  isZero * x === 0  -- If x is not zero, isZero is zero

  return isZero

My remaining wishes about Clean

It's cumbersome having to remember the different kinds of circuits: Circuit, ElaboratedCircuit, Subcircuit, FormalCircuit, FormalAssertion and FormalGeneralCircuit.

When I use a sub-circuit, I see (something_complicated).output in the goal state instead of just a single variable for the output of the sub-circuit. This doesn't usually matter because I have the specifications of the subcircuits telling me things about the (something_complicated).output. Since I never need to look into the structure of the complicated term, I could just see a variable instead of this.

Me vs Claude Code

I'm better than Claude Code at working with Clean.

Some dormant projects

Coda and risc0-lean4 have some Lean code for arithmetic circuits. The last updates are years ago, so I didn't include these projects in the comparison.

Future

What's coming in this field? In the short term, more frameworks will appear. Somebody will come up with the idea that polynomial circuits are like effectful lenses/relation-oriented programming/representation theory. In the mid-term, except for hand-craft optimized circuits, people will stop writing circuits themselves. Most polynomial circuits will be automatically generated. Some formal verification techniques will be used with less and less manual intervention. Evaluating results of verification efforts will remain a challenge.

zkSecurity offers auditing, research, and development services for cryptographic systems including zero-knowledge proofs, MPCs, FHE, and consensus protocols.

Learn more →

Share This Article

Latest Posts

Sigma dance: commit, challenge, respond

teddav November 18, 2025
educative zk

Learn the fundamentals of Σ-protocols through the classic Schnorr protocol, exploring the three-step dance of commit, challenge, and respond. This post walks through knowledge soundness and witness extraction, then shows how to compose Sigma proofs with AND/OR logic and Pedersen commitments. See working SageMath implementations, discover how Fiat-Shamir transforms interactive proofs into non-interactive signatures, and understand the deeper mathematical structure as proofs of knowledge of homomorphism pre-images.

Circle STARKs: Part IV, Arithmetizing Circles

Varun Thakore November 17, 2025
educative zk fri

In this final part of our series on Circle STARKs, we tie together concepts from Mersenne prime fields, circle curves and bivariate polynomials to showcase a comprehensive Circle STARK protocol. We detail the process of arithmetization over the circle curve, introducing Circle FRI as a low-degree test and walk through the complete Circle STARK construction. Readers will explore how trace commitments, constraint batching and low-degree proofs combine for efficient verifiable computation, delving into the nuances of proof validity and security analysis.

Proximity Gaps: What Happened and How Does It Affect our SNARKs

Nicolas Mohnblatt November 14, 2025
educative security zk

A series of recent papers just disproved the proximity gaps conjecture, which has everyone wondering if hash-based SNARKs are in trouble. We break down what actually happened using some helpful visuals—think of it as understanding which parameter choices are safe versus which ones are now confirmed to be risky. The post walks you through the different security zones (proven safe, conjectured safe, and definitely not safe), explains how these new results connect to other open math problems, and shows what it means for real-world SNARKs in terms of proof sizes and performance trade-offs.

More to Explore

Become a Halo2 Hero: Master Zero-Knowledge Proofs with Our New Course

Mathias Hall-Andersen November 14, 2024
educative zk halo2 plonk

We're teaming up with the Zircuit team to bring you a new course on Halo2 development that's perfect for Rust developers eager to dive into creating Halo2 circuits from scratch. No need to be a cryptographer or have prior knowledge of Halo2, PlonK, or zkSNARKs—our course starts with the basics and guides you through building increasingly complex circuits. By the end, you'll be a Halo Hero! Plus, you'll have access to complete, runnable code examples on GitHub. Ready to start your Halo2 journey? Check it out!

Public report of auditing Penumbra's circuits

ZK/SEC August 24, 2023
security zk audit

We conducted an audit of Penumbra's main circuits and found eight issues, including the critical "double spend" and "double vote" bugs, which the Penumbra team promptly fixed. Our findings highlight Penumbra's robust documentation and code testing. Readers will get insights into how Penumbra uses zero-knowledge proofs for privacy, its decentralized exchange features, and its governance model. The post also provides detailed pseudocode for various cryptographic protocols, emphasizing how Penumbra ensures secure and private transactions. It's a deep dive into the technical details for those intrigued by privacy-focused blockchain technologies.

Private delegated computation is here, and there will be bugs!

ZK/SEC May 30, 2023
announcement

Dive into the intriguing world of zero-knowledge cryptography with us as we unravel its connection to trusted and confidential computing. Learn why this tech is making us rethink security like never before. From the evolution of private and delegated computing to the revolutionary power of zero-knowledge proofs, we'll explore how these advancements are shaping industries beyond cryptocurrencies. With big players like Microsoft jumping on board and the potential for new applications, zero-knowledge cryptography is poised to redefine digital trust. Join us on this journey as we launch our new security consultancy, designed to navigate and secure this cutting-edge landscape.
View all articles