This post is about some major updates to Clean, the Lean circuit verification framework. We show how we are expanding from isolated gadgets to end-to-end verification of multi-AIR systems, such as zkVMs. The work builds on a new Clean primitive called Channel which models cross-table interactions.

You can watch the talk we gave at ZKProof 8 in Rome, or read on for the blog version.

What is Clean?

Clean is an embedded DSL for zk circuits in Lean4. Here is the popular isZero circuit:

def isZero : FormalCircuit F field field where
  /-- `main` is the circuit itself -/
  main (x : Expression F) := do
    let z ← witness fun env =>
      if env x ≠ 0 then (env x)⁻¹ else 0
     -- if x = 0 then b = 1
    let b <== 1 - x * z
      -- if x ≠ 0 then b = 0
    b * x === 0
    return b

  /-- `Spec` captures the high-level meaning of the circuit -/
  Spec (x : F) (b : F) :=
    b = (if x = 0 then 1 else 0)

  /-- `soundness` proves that the `Spec` follows from constraints
    (independently of witness assignment) -/
  soundness := by circuit_proof_all

  /-- `completeness` proves that if the prover uses the circuit's honest
    witness assignment, the constraints are satisfied. -/
  completeness := by circuit_proof_all

As you can see, Clean provides a circuit frontend with primitives like === (equality constraint) and witness, as well as a language of circuit correctness (soundness and completeness properties). It is designed such that developers write reusable gadgets in tandem with their spec, and with proofs of correctness vs the spec.

Note that the code above is just Lean, it is not a standalone DSL and has no special compiler. The circuit frontend is written in a Lean monad (do notation). We added a few syntax extensions like === and <== (easy to do in Lean itself), but fundamentally Clean is just a library, with the full expressivity of Lean available to build abstractions.

Clean comes with some automation designed to unwrap our framework boilerplate and make trivial statements easy to prove, such as the circuit_proof_all tactic which, in the simple example above, makes the proofs a one-liner.

Channels in Clean

The new work in Clean is about scaling from a single circuit to a system of circuits. This is the shape of modern proof systems, especially zkVMs: the prover does not usually produce one monolithic trace. Instead, there are many tables, each with its own local constraints, and the tables communicate through multiset equality arguments.

Different projects use different names for this architecture. The S-two whitepaper calls it "flat AIR", Binius describes it as the M3 architecture, and OpenVM uses the same pattern and calls it AIR with interactions. The common idea is:

• a component is a table with a local circuit that applies to every row,
• local constraints only talk about one table at a time,
• cross-table claims are enforced by multiset equality arguments.

Clean models those multiset equality arguments as Channels.

structure Channel (F : Type) (Message : TypeMap) [ProvableType Message] where
  -- just a `Message` type and a string
  name : String
  -- discussed later
  Guarantees (message : Message F) (data : ProverData F) : Prop

A channel is a named space of messages. A circuit can push messages into it, or pull messages out of it. At the proof-system level, the channel is balanced when every pulled message is matched by a pushed message with the same multiplicity. That abstraction covers lookup tables, the PLONK permutation argument, and the cross-table interactions used by zkVMs.

The first design question is how a local circuit should reason about a pull. Suppose a circuit wants to range-check a value to be a byte, using a lookup. Doing so, translated to channel language, means pulling that value from a byte channel.

def BytesChannel : Channel (F p) field where
  name := "bytes"
  Guarantees msg _ := msg.val < 256

The circuit performing the range check will probably need the property < 256 somewhere in its soundness argument. A tempting model is therefore to say: when a circuit pulls from a channel, we just assume the channel's guarantee. Assumptions from channel interactions cannot be proved from local constraints, but they are usually necessary to make local proofs work.

Equally important is the other side of the interaction: a circuit that pushes to a channel has to prove the guarantee for the message it pushes. Local soundness therefore has two channel-related parts:

• pulls become assumptions,
• pushes become proof obligations.

As a concrete example, this 8-bit addition chip can assume the byte guarantee on z while it has to prove the guarantee of the Add8Channel which it pushes (x,y,z) to:

/-- Proves x + y = z (mod 256) -/
def add8 : GeneralFormalCircuit (F p) Add8Inputs unit where
  main | { x, y, z, m } => do
    -- range-check z using the bytes channel
    -- (x and y are guaranteed to be range-checked from earlier interactions)
    BytesChannel.pull z
    -- witness the output carry
    let carry ← witness fun env => floorDiv (env (x + y)) 256
    assertBool carry
    -- assert correctness
    x + y === z + carry * 256
    -- emit to the add8 channel with multiplicity `m`
    Add8Channel.emit m (x, y, z)

Local proofs, global meaning

Consider an ensemble of AIRs which features both the bytes table and the add8 component as a chip that is used by other tables. What does soundness mean for such an ensemble, as a whole?

Our answer is that global soundness must make no mention of extra assumptions like BytesChannel.Guarantees. Instead, it can only assume that all channels in the ensemble are balanced, which is what the proof system enforces. Here is our Lean definition:

/--
The raw "statement" that a proof about an ensemble makes. Could also be called "relation".
-/
def Statement (ens : Ensemble F PublicIO) (publicInput : PublicIO F) : Prop :=
  ∃ witness : EnsembleWitness ens,
    witness.publicInput = publicInput ∧
    witness.Constraints ∧
    witness.BalancedChannels

/-- Soundness: assumptions plus the raw statement imply the spec. -/
def Soundness (ens : Ensemble F PublicIO) (Assumptions Spec : PublicIO F → Prop) : Prop :=
  ∀ publicInput, Assumptions publicInput → ens.Statement publicInput → Spec publicInput

When lifting from local to global soundness, we have to prove local assumptions from channel balance, in order to discard these assumptions. Roughly speaking, this works because, by balance, any pull is accompanied by a push of the same message. For the push, we actually proved the same assumption in the component that pushed, assuming that component's constraints. And so the previously missing assumption follows for the pull. As long as this reasoning chain doesn't descend indefinitely, but ends at a base case that makes no further assumptions, we can prove all local assumptions from local constraints plus global balance.

Luckily, users of Clean will not have to make these kinds of arguments, as all the hard parts of the local-to-global lift are proved generically at the library level. Users only have to assemble AIRs "in the right way" such that our framework can rule out infinite reasoning cycles.

Notably, the system of local assumptions lets gadgets stay self-contained: The add8 circuit is proved once, against the abstract guarantee of the byte channel. It doesn't need to know about which multi-AIR ensemble it might be included, and doesn't need to reason about any global properties of that ensemble.

Another nice property is that, since the Channel.Guarantees are not mentioned in global soundness, they are untrusted code: We can pick them however we like to make our local proofs easier. Auditors don't have to worry about them (just about the global Assumptions and Spec).

A Fibonacci ensemble

As a toy example that demonstrates all the ideas, we built a small Fibonacci VM. It has three channels:

• bytes, a static lookup channel containing all 8-bit values,
• add8, an addition channel for 8-bit addition,
• fibonacci, a state channel for the Fibonacci transition table, which computes "Fibonacci modulo 256".

The dependency structure is zkVM-like: The byte table pushes all byte values. The add8 table pulls from BytesChannel, checks 8-bit addition, and pushes into the Add8Channel. The Fibonacci transition table pulls from FibonacciChannel to get the last state, pulls from Add8Channel to justify the arithmetic step, and pushes new state to FibonacciChannel.

In Clean, the final assembly looks like this:

def fibonacciEnsemble := SoundEnsemble.empty (F p) fieldTriple
  |>.addTable ⟨ pushBytes ⟩
    (by simp [circuit_norm, pushBytes]) (by simp [circuit_norm, pushBytes])
  |>.addFinishedChannel BytesChannel.toRaw
  |>.addTable ⟨ add8 ⟩
    (by simp [circuit_norm, add8]) (by simp [circuit_norm, add8])
  |>.addFinishedChannel Add8Channel.toRaw
  |>.addVm fibonacciVm
    (by simp [circuit_norm, fibonacciVm, add8, pushBytes, Add8Channel, FibonacciChannel])
    (by simp [circuit_norm, fibonacciVm, fib8, fibonacciVerifier])
    (by simp [circuit_norm, fibonacciVm, fib8, fibonacciVerifier, Add8Channel, FibonacciChannel])
  |>.toFormal _ (fun _ _ => True)
    (by simp [circuit_norm, fibonacciVm, add8, pushBytes, fib8])

This is where the local-to-global lift happens from the user perspective: we add tables and channels and have to do so in the right order so that Clean can guarantee soundness at every step. A channel can be marked as "finished" when none of the tables so far have pulled from it, and after marked finished, no table can push to it (so, there is a strict hierarchy that prevents cycles).

There are some easy inline proofs (by simp [circuit_norm, ...]) that establish properties like "this new table does not push to any of the finished channels".

The zkVM case

Near the end, there is a step .addVm which can be used with a list of components all using a single "VM state channel". This is a channel that does not follow a hierarchical structure: it can be pulled from and pushed to within the same table. For Fibonacci, a step pulls the current state (n, x, y) and pushes the next state (n + 1, y, x + y).

The theory for VM state channels is more complicated than for lookup-like channels. There may be a closed cycle of transitions in the trace. In such a cycle, every row's guarantee is justified by another row's guarantee, but there is no base case. The local table statement "every row is a valid transition" is not enough, by itself, to rule out these cycles.

Fortunately, this is not the statement we actually need for a VM. The public IO of the VM gives us the base case. The verifier table pushes the initial state and pulls the final state. Channel balance forces the initial and final state to live in the same cycle of transitions. Since the initial state guarantee is known, Clean can follow the chain of transitions and conclude the guarantee of the final state.

So the global theorem for VMs is slightly different from the theorem for ordinary lookup hierarchies. We do not prove that every state interaction in the trace has an independent external meaning. We prove the VM statement that matters: there exists a valid trace from the public initial state to the public final state.

Again, this proof burden does not show up at the user level because it is handled in a generic way by Clean.

Why completeness

There is one final trap, and it is easy to miss if we only talk about soundness.

Imagine a channel whose guarantee is literally false:

def FalseChannel : Channel (F p) unit where
  name := "false"
  Guarantees _ _ := False

def falseCircuit : GeneralFormalCircuit (F p) unit unit where
  main _ := FalseChannel.pull ()
  Spec _ _ _ := False
  soundness := by circuit_proof_start [FalseChannel]

Locally, this circuit is sound: if the pulled message satisfies the channel guarantee, then False follows. Globally, we can build an ensemble around it, and funnily enough, the ensemble is sound as well:

def falseEnsemble := SoundEnsemble.empty (F p) unit
  |>.addFinishedChannel FalseChannel.toRaw
  |>.addTable ⟨ falseCircuit ⟩
    (by simp [circuit_norm, falseCircuit]) (by simp [circuit_norm, falseCircuit])

The catch is that we added no table that pushes to the channel (there can be none). So channel balance can never be satisfied. The ensemble is sound, but meaningless since the soundness theorem has an unsatisfiable assumption.

This illustrates why Clean treats completeness as a first-class part of circuit correctness. Completeness says that honest execution can actually produce a trace that satisfies the constraints. Without completeness, it is too easy to prove a theorem whose assumptions are impossible.

Proving the local-to-global lift for completeness in Clean is future work.

Where this is going

Channels give Clean a way to keep circuit reasoning local while still proving global statements about multi-table systems. Gadget authors can prove small components against abstract channel guarantees. Ensemble authors can combine components and get an end-to-end theorem for the whole AIR layout.

This is the direction Clean is moving in: from verified gadgets to verified zkVMs.