.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
Marco Stronati has been working in blockchain research and development since 2018. He finds Zero Knowledge proof system incredibly promising and he is frustrated that it’s still so hard to write circu
Now hiring!
•
CLAP is a work-in-progress compiler for zero-knowledge circuits, funded by the Aptos Foundation to support the verification of Aptos Keyless circuits. It explores an approach where circuits can be written in Lean and formally verify them against a specification, without relying on a separate DSL or embedding style that adds extra proof overhead.
CLAP compiles these programs into constraint systems and witness generators through a semantics-preserving pipeline, so properties proved at the source level carry through to the final system. This effectively takes verified logic down to the constraint level. CLAP also introduces certified optimizations at the program level, allowing circuits to be written more naturally while preserving correctness and enabling safer manual optimization.
In ongoing work on Aptos Keyless, this approach has already begun to surface opportunities to reduce circuit size compared to the original Circom implementation. CLAP moves toward a workflow where verification, compilation, and optimization are unified into a single, consistent process.
The gap between a circuit specification and its constraint system is where bugs live. Testing narrows that gap. Formal verification aims to close it. Writing circuits in a proof assistant like Lean allows to prove the implementation respects the specification.
However it is quite challenging to write a circuit at the right level of abstraction. On one side verification benefits from abstraction. On the other, efficient constraint generation benefits from a more detailed description of the computation. If compilation details leak into the source, the circuit becomes harder to reason about and harder to prove correct.
CLAP is designed to address that problem. It is not a DSL nor a separate language. A CLAP circuit is simply Lean code. The only restriction is that the Lean program should describe a computation suitable for an arithmentic circuit (e.g. no general recursion). Within that subset, the user writes a function. The meta compiler derives a constraint system from it.
Embedding a DSL into an existing host language is the standard approach, and for good reason. The host language provides types, tooling, and an ecosystem. Rust gives a well-understood, widely adopted base. OCaml and Haskell give stronger types and better support for the state monads these embeddings typically require.
An ancestor of CLAP was embedded in OCaml in 2022 to build Plonkish circuits. A Rust variant followed in 2024, described in the arXiv paper. Halo2 and other popular systems take a similar approach.
These embeddings all share the same problem: carrying around a state monad with the constraint system being built and manually managing the variables (or wires) used in the constraints. The resulting state monad must be kept well-formed at all times: variables correctly allocated, constraints consistent with the program being built. While this management can be done correctly with some reasonable software engineering, proving its correctness is much harder.
Several projects have built ZK circuit DSLs in Lean, following our same motivation: verify the circuits as well as the compilation. However they have followed the classic embedding strategy, which gets in the way of proving.
Proof assistants based on dependent type theory, such as Lean and Rocq, are built on the Curry-Howard correspondence: a theorem is a type, and a proof is a program inhabiting that type.
In order to write a proof, these systems actually need to build a program, and they provide very sophisticated meta-programming infrastructure to facilitate that task.
CLAP uses this infrastructure to take a user program and, through a series of transformations and optimizations, lower it toward an equivalent constraint system. The source program contains no trace of the compiler: no state monad, no variable bookkeeping.
Because the specification is free from embedding artifacts, it avoids additional proof obligations introduced by the embedding.
The main restrictions for a Lean program to be considered a circuit are:
Option Unit, where none represents the circuit failing a check and some() an accepting run.
For a simple example, consider the following specification, which computes the product of the elements of a vector v and checks it corresponds to the expected result.
def spec (v : Vector (F p) 2) (expected : F p) : Prop :=
v.foldl (fun acc x ↦ acc * x) 1 = expected
We can implement this abstract specification as the following executable (and compilable) circuit.
def circuit (v : Vector (F p) 2) (expected : F p) : Option Unit := do
let prod ← v.foldlM (fun prod x ↦ share (x * prod)) 1
F.assertEq prod expected
We can use common Lean functions such as foldlM, our own function assertEq that checks equality of two field elements and a basic operand share : F p → Option (F p) that helps to break up large expressions so that the degree remains manageable.
This implementation is remarkably close to its specification with only a couple of details related to compilation.
share constructor is a compiler hint, but its definition is just the identity so it does not get in the way of proving. Expression splitting is not currently automated and must be specified explicitly. This is expected to be handled within the compiler in future versions.
We can proceed to prove an equivalence between specification and implementation and we can observe that this is just a Lean exercise. No circuit related knowledge is needed to follow this this proof. It reduces to a standard Lean argument.
lemma equiv (v : Vector (ZMod p) 2) : circuit v = some () ↔ spec v
Working with Vectors and monadic code has of course its own challenges, but these are core aspects of the semantics of circuits, and can be dealt with using standard Lean infrastructure such as mvcgen. CLAP does not introduce additional obligations beyond those already present in the specification.
The compiler is implemented using Lean’s meta-programming infrastructure and takes advantage of its symbolic computation features, including simp , to simplify the program. Vectors need to be handled carefully to make sure that the size information allows simp to fully reduce a circuit. A set of basic operators, such as eq0 and share, are marked irreducible, so that simp does not unfold them. Compilation stops when the program has been fully reduced to a linear sequence of these operators.At this stage, there is still no constraint system and no witness generator.
def circuit_reduced (v : Vector (F p) 2) (expected : F p) : Option Unit := do
let prod0 ← share (v[0] * 1)
let prod ← share (v[1] * prod0)
eq0 (prod - expected)
The reduced circuit is then transformed into a Constraint System and a Witness Generator.The operator eq0 simply checks if an expression is equal to zero, which can be compiled by introducing a constraint. This means that eq0 is already "compiled" and to obtain a constraint system we need to reduce all other operators to eq0. In the case of share, we can turn let x ← share e into eq0 (x - e).
When compiling to constraint system, all the irreducible operators are broken into a simple sequence of constraints (the eq0 operator) and all necessary auxiliary inputs are introduced.
def ex_cs (v : Vector (F p) 2) (expected : F p) : F p → F p → Option Unit :=
fun prod0 prod ↦ do
eq0 (v[0] * 1 - prod0)
eq0 (v[1] * prod0 - prod)
eq0 (prod - expected)
Similarly the witness generator is defined as a function that takes the same inputs as the circuit and produces a list of auxiliary inputs, the same that the constraint system expects.
def ex_wg (v : Vector (F p) 2) (expected : F p) : List (F p) :=
let prod0 := v[0] * 1
let prod := v[1] * prod0
[prod0,prod]
The constraint system is proved sound with respect to the circuit.The constraint system, joined with the witness generator, is proved complete with respect to the circuit.
Inspection of circuit_reduced reveals several opportunities for optimization. First, we can remove the multiplication by 1, which is generally already handled by simp during reduction. Second, the shares are redundant and can be eliminated by inlining, yielding the following.
def circuit_opt (v : Vector (F p) 2) (expected : F p) : Option Unit := do
eq0 (v[0] * v[1] - expected)
In this simple example, the vector has only two elements, so the expression can be inlined safely. With larger circuits, expressions often need to be split with share to keep the degree compatible with R1CS.However this example illustrates the opportunities to optimize our circuits before they are lowered to constraint system and witness generator. The optimization we are exploring are relatively straightforward to reason about and show promise in reducing circuit size. This is still work in progress but we should have numbers soon.
These kind of transformations are quite complex to do in the classic embedding style as the constraint system is already built. This means that most of the original program structure is lost, it is hard to manipulate explicit variables and the same has to be done for the witness generator without introducing inconsistencies. To the best of our knowledge, this combination of automatic optimizations and formal guarantees is not widely explored in existing systems.
This example shows why optimizing before lowering to a constraint system matters. At this stage, CLAP can still use the structure of the original program. That makes some transformations easier to express, easier to prove correct, and they propagate to both the constraint system and witness generator.
This remains work in progress, and we expect to share more concrete results as the compiler matures.
The current iteration of CLAP in Lean has been made possible by the Aptos Foundation. The goal is to rewrite the Circom circuits used in Aptos Keyless in CLAP, in order to eliminate soundness bugs and prove functional properties of the circuits, for example the correct parsing of JWT payloads.
Keyless contains a number of components of general interest which may apply to a number of other projects, such as SHA2-256 and Poseidon, as well as RSA verification.
It should be noted that while Keyless uses R1CS as an arithmetization format, as so this is the first backend we developed, CLAP's pipeline can be easily adapted to other formats. Indeed both previous versions of CLAP targeted PlonKish.
We have currently re-written the entirety of Keyless in Clap. At this stage, the circuits have been tested, but are not yet fully verified. We are in the process, on one side, to write specifications for them and, on the other, to compile them down to constraint systems.
The size of the projects, that currently produces 1.4M constraints using Circom, has been a challenge. After a few iterations we are currently building a version of the compiler that should be able to scale accordingly.
We have made great progress in proving soundness and completeness for all the basic gates. In particular num2bits which is used to convert between field elements and their bit representation and fpMul, which performs multiplication modulo a large prime inside RSA verification.
A note on the previous CLAP paper: The 2024 arXiv paper describes a Rust-based approach to circuit DSL embedding, also named CLAP. That work and this project share some high-level ideas but are technically distinct. The Lean implementation is a deep redesign: the technique, the architecture, and the formal foundations differ. A new paper is in preparation.
The Leading Engineers of Blockchain Infrastructure
Nethermind © 2026
.svg)