Zero-knowledge virtual machines (zkVMs) let developers prove that an arbitrary program ran correctly, without a prover-writer ever touching a proving circuit. That convenience comes at a cost: every RISC-V instruction the guest program executes adds to the work the prover has to do. A general-purpose zkVM interpreter re-derives the same decode-and-dispatch bookkeeping for every single instruction, even when a whole sequence of instructions is doing one conceptually simple thing, like the inner loop of a hash function.

powdr is an open-source compiler toolkit built on top of zkVMs, mainly OpenVM, with experimental support for SP1 as well, that attacks this problem automatically. Certora has been working with the powdr team on autoprecompiles: powdr's mechanism for auto-generating custom circuits for hot code. More specifically, we've been formally verifying that this optimization never changes what a program computes.

This post explains what autoprecompiles are, how we define and check their correctness, and what our verifier found on two real-world workloads: a Keccak precompile and an execution trace from Reth.

What powdr does

If the idea of autoprecompiles sounds familiar, it should: powdr runs a fairly traditional compiler optimization, something like instruction fusion or inlining across a hot loop body. The difference: the "instructions" are circuit constraints, and the artifact it produces is a proving circuit instead of machine code.

Given a guest program, powdr profiles its execution to find hot basic blocks: straight-line runs of instructions with no branches. For each block, it builds a single constraint system by inlining the existing circuits for every instruction in the block. powdr's circuits work over a moderate-sized finite field, mostly the BabyBear field used by OpenVM. They consist of arithmetic equalities together with bus interactions. OpenVM’s circuits use buses to talk to each other for memory, execution ordering, range checks, bitwise lookups, and so on. This mechanism comes directly from the underlying zkVM and powdr merely mimics the underlying semantics to enable faithful optimizations.

The combined system for a whole block is large and full of redundancy: opcode-selector logic that is now known at compile time, intermediate registers that only existed to hand a value from one instruction to the next, memory writes that are immediately overwritten. Powdr’s optimizer pipeline repeatedly simplifies the merged system. It substitutes in values once they're known, cancels out memory writes that are immediately overwritten, drops variables nothing else in the circuit still depends on, and more. It keeps going until the system stabilizes. The result, the autoprecompile (APC), is emitted as a single, fixed circuit that OpenVM runs in place of the entire original instruction sequence.

This is a different route to the same destination most zkVMs reach today via hand-written precompiles: bespoke circuits for specific operations like Keccak or pairing checks. Hand-written precompiles work, but they come at a cost. Every one has to be designed, implemented, and audited by circuit engineers, redone for every proving backend, and it roughly doubles the code a team has to maintain: the circuit logic, and the witness-generation logic that has to agree with it perfectly. powdr's autoprecompiles aim at similar performance without that manual, per-backend effort.

The payoff is that the prover pays once for a small, specialized circuit instead of paying, instruction by instruction, for a general-purpose interpreter loop. powdr's own benchmarks report reductions in the 2.5–6x range on individual workloads for the number of constraints, which is supposed to be a decent proxy for the expected proof time. The auto-generated circuits already approach what hand-written precompiles achieve.

Why this needs formal verification

All of that simplification happens automatically, block by block, driven by a general-purpose rewrite engine. That makes it closer to a compiler's optimizer than to a single hand-checked circuit. It is exactly the kind of code where a correctness bug is easy to introduce and easy to miss: a rewrite rule that is sound for the cases the test suite happens to cover can still be wrong for some other combination of instructions.

To see why this matters, it helps to remember what a zkVM proof is for. Something like Reth's execution logic, or a Keccak hash, gets run inside the zkVM for one reason: so a verifier can accept a short proof instead of re-executing the computation itself. That verifier is often a smart contract on a blockchain, for example in the context of a ZK rollup. It trusts the circuit completely: if the circuit is willing to accept a witness, the verifier accepts the proof. So a bug in an autoprecompile's circuit isn't a crash, or a wrong output on screen. It's a hole in what the whole cryptographic argument is supposed to guarantee, and that hole can go either direction:

• The circuit accepts too much (a soundness bug). If the optimized circuit accepts a witness that doesn't correspond to any real execution of the original instructions, someone can construct that witness on purpose. A rollup would accept incorrect state transitions, this is the "mint tokens out of thin air" class of bug: a prover convinces the on-chain verifier that an invalid transaction or block was executed correctly, because the accelerated circuit for one of its precompiles was slightly too permissive.
  If the circuit is used for ZK, like in a zkRollup, this is even more dangerous, because the witness is fully hidden, so the invalid transition is provably undetectable, even if you have a hypothesis about what invalid transition occurred.
• The circuit accepts too little (a completeness bug). If the optimized circuit can no longer find a satisfying witness for some execution the original instructions legitimately allowed, that's not a security hole but a liveness problem: an honest transaction that should be provable suddenly isn't, and the chain or rollup gets stuck on it.

Neither failure mode is something you want to discover after a precompile was shipped. So instead of trusting the optimizer, we built a verifier. It independently checks, for every optimization step, that the circuit before and after are equivalent.

Our approach

To verify an autoprecompile, we consider each optimization step individually and take two constraint systems for each: the one just before the pass ran, and the one just after. Both are the same kind of object described above, algebraic constraints plus bus interactions. We ask whether the two are equivalent.

powdr's optimizer runs as a pipeline of about a dozen passes, executed until fixed-point, applied to each basic block individually. One pass, for example, merges the "which instruction runs next" bookkeeping between two instructions that just got fused together; another employs powdr's own internal solver to pin certain variables down to constants and substitutes them in; a third cancels out a memory write that's overwritten before anything reads it; a fourth prunes variables that nothing else in the circuit still depends on. These passes run repeatedly until the system stops shrinking. Rather than trying to verify the whole optimizer at once, we check every consecutive pair of intermediate circuits independently: pass n's output circuit must be equivalent to pass n+1's output circuit. If every link in that chain holds, the final autoprecompile is equivalent to the unoptimized block by transitivity.

What "equivalent" means. We split equivalence into two directional obligations, mirroring the standard soundness/completeness split used for verified compiler and ZKP-correctness arguments:

• Soundness: every behavior the optimized circuit accepts corresponds to a real behavior of the original circuit.
• Completeness: every behavior the original circuit accepts is still accepted by the optimized circuit.

Both are stated over the circuit's external interface: the values sent and received on stateful buses like memory and execution order. Neither looks at internal signals. Two circuits can use completely different internal variables and still be equivalent, as long as they exchange the same values on those buses. Two circuits that use different stateless lookup tables (bitwise, range checks) are also treated as equivalent, since a "table sink" circuit can absorb any legal interaction with those buses. This lets the verifier confirm the intent of an optimization pass ("the memory traffic is unchanged") without getting distracted by superficial restructuring of the internals.

Concretely, soundness is the statement: for every satisfying assignment of the optimized circuit's variables, there exists an efficiently computable satisfying assignment of the original circuit's variables that produces the same effect on the stateful buses. As a formula: ∀ (optimized-circuit variables), optimized-constraints ⟹ ∃ (original-circuit variables), original-constraints ∧ same bus effect. Completeness is the same statement with the two circuits swapped: ∀ (original-circuit variables), original-constraints ⟹ ∃ (optimized-circuit variables), optimized-constraints ∧ same bus effect.

We don't ask the solver to prove either implication directly; we negate it and check the result for unsatisfiability, the usual "assumptions ∧ ¬goal" shape. For soundness we assert the optimized circuit's constraints as ordinary (existential) variables, together with a universally-quantified assertion that no assignment of the original circuit's variables reproduces the same effect:

optimized-constraints ∧ ∀(original-circuit variables) (¬original-constraints ∨ ¬same bus effect)

If that combined formula is unsatisfiable, no counterexample exists, and soundness holds. If it's satisfiable, the satisfying assignment is a concrete counterexample: an assignment to the optimized circuit that the original circuit can't match, which is invaluable for debugging an optimizer regression. Completeness works the same way with the two circuits' roles reversed.

The formula we aim to check is thus universally quantified: over the original circuit's variables when checking soundness, and over the optimized circuit's variables when checking completeness. Z3, the mature, open-source SMT solver from Microsoft Research, can solve quantified formulas directly, but in practice it's substantially slower at that than at quantifier-free formulas, which is what it was originally built for. So before handing anything to the solver, we eliminate the quantifier ourselves using domain-specific knowledge.

The main tool for that is skolemization: we try to build an explicit assignment for each universally-quantified variable, a concrete expression in terms of the other, already free ("ground") variables, that the quantified variable must equal given the surrounding constraints. This expression is called a skolem, and once we substitute that skolem for the targeted quantified variable it is eliminated: a quantified variable is removed in favor of a quantifier-free expression. Luckily, this almost always works for all of the quantified variables that show up in practice using pretty simple techniques, so we're left with a fully quantifier-free (QF) formula.

Nothing forces the skolem we substitute for a quantified variable to be the right one, and this is worth being precise about. If we derive a wrong skolem, the formula can spuriously become satisfiable: Z3 hands back a "counterexample" that isn't a real one, just an artifact of a bad skolem. That's a false positive, not a soundness bug in powdr. Fortunately, we’re able to avoid bad skolems entirely, by basing our skolem-construction on what powdr's optimizer does internally, not by guessing blindly. And even if we make a mistake, a wrong skolem can never cause a bad circuit pair to be verified but only claim a good circuit pair to be not equivalent; manual inspection of such a situation would then reveal that the skolem was incorrect.

Skolemization plus a handful of other standard simplifications (rewriting modular-arithmetic expressions into a normal form, propagating known bounds and bitmasks, and a few more in that vein) is the pipeline we run before anything reaches the solver. What's left goes to Z3. We didn't write our own solver; we apply rather standard simplifications and then drive an off-the-shelf one. We also occasionally split large formulas into smaller, independently solvable chucks by exploiting disjunctions.

This has been roughly an eight-month effort, run jointly with the powdr team as their optimizer itself kept evolving underneath us. We consider the verifier a research prototype rather than a finished, hardened tool. It reliably handles full production-scale workloads (see below), but it hasn't been packaged for outside use. We're also continuing to look at ways to increase confidence in the approach itself: for instance, we've started formalizing pieces of the underlying quantifier-elimination argument (the skolemization step) in Lean, as an independent, machine-checked cross-check of our own reasoning.

Alternative encodings, and a few tricks that mattered

Most of the practical performance work behind the results below didn't happen at the level of the circuit-level equivalence definition. It happened in how we translate a circuit into a formula in the first place. A good deal of it comes down to one recurring idea: wherever we can, we hand Z3 a formula it can close with equality reasoning, just noticing that two things are equal, rather than one it has to grind through with real, often modular or nonlinear, arithmetic reasoning. Equality reasoning is close to free for an SMT solver. Arithmetic reasoning over a 31-bit prime field is where it can get stuck. Two things mattered far more than the rest in pursuing that: how we encode the memory bus, and a handful of specific rewrite rules that turned expensive arithmetic queries into cheap equality ones.

Encoding the memory bus. The single encoding choice that mattered most was how to represent the memory bus. We went through three different designs. The first modeled memory literally as an SMT array: one array per data variable, indexed by address space and pointer, updated by an explicit read/write at every memory-bus interaction. It's the textbook encoding, and the cleanest to state, but it was fragile and didn't scale very well. Z3's internal array solver naively has to relate every store to every read that might alias it. On our circuits, that blew up to 70,000–160,000 possible relationships  per query, with solve time scaling linearly in that count. We eventually dropped this encoding entirely.

Its replacement is our default today. It encodes the underlying permutation check without any array theory: a boolean "this access matches that access" variable for every pair of accesses that could plausibly alias (after our customized alias analysis prunes the obviously-impossible pairs), an "exactly one match" constraint per access, and a direct equality on each matched pair. That pairwise matching search is still real work, though, at least when we can not statically pin all matches.

We added a third, cheaper option too, which seems very specialized, but actually applies to most of powdr’s pipeline. Consider a case where the two circuits have the same number of memory operations, and our static pre-analysis can prove that the two circuits have the same pointers. In this case, we skip trying to understand within-circuit aliasing at all. Instead, we simply verify that each write-pair in the circuits have equal writes, assuming all prior reads are equal. This is a great example of the kind of equality reasoning that SMT is good at, and it entirely eliminates any need to reason about aliasing. And, it actually applies to most optimization steps in powdr, because most steps do not affect memory accesses. 

The most important rewrites. Below the encoding layer, most of the gains came from a rather short list of rewrite rules applied to the formula before it ever reaches Z3. A few stood out as more than bookkeeping:

• Factoring modular polynomials. Circuits are full of expressions like bit * (bit - 1) = 0, the standard gadget for constraining a field element to be exactly 0 or 1. Left as-is, that's a nonlinear equation modulo a 31-bit prime, and it forces Z3 into genuinely hard nonlinear reasoning. We instead factor the polynomial, using FLINT, an off-the-shelf number-theory library. We rewrite it as an explicit disjunction over its roots together with range constraints, (bit = 0 ∨ bit = 1) ∧ bit < 2 in this example. This rewrite trades a hard arithmetic constraint for a handful of plain equalities Z3 case-splits on and then uses for constant propagation, and a range constraint that Z3 can use for interval reasoning. The effect on real Z3 calls was substantial. One call that had been timing out past 70 seconds solved in 0.06 seconds once this rewrite, and a companion fix nearby, landed. Another dropped from 45–61 seconds to 1.3–1.5 seconds, roughly a 35x improvement.
• Bitwise operations without bit-blasting. Not every trick fits the equality theme. This one is about avoiding a different kind of blowup. AND/OR/XOR show up in circuits as opaque operations over byte-sized values. The textbook way to reason about them in an SMT solver is to expand every operand bit by bit. That's a combinatorial disaster at circuit scale. We instead attach a small set of linear arithmetic identities that pin down the same values without ever expanding to bits: for example x + y = xor(x,y) + 2·and(x,y), together with simple bounds like 0 ≤ and(x,y) ≤ min(x,y). That lets Z3 reason about bitwise values as ordinary bounded integers instead.
• Turning off one of Z3's own defaults. Z3's built-in solve-eqs tactic will, by default, "help" by eliminating modular-arithmetic terms through a fresh witness variable for the quotient. On our formulas, that backfired. Those witnesses are themselves nonlinear, and they multiply across the rest of the goal. In one case, that turned a 1.5-second check into a 60-second timeout. We disable that specific behavior. Instead we do our own, more targeted modular-arithmetic rewriting: the same family of rewrite mentioned earlier, which turns a·x + b ≡ 0 (mod p) directly into the equality x = -b/a (mod p). That way Z3 never has to search for it via nonlinear arithmetic of its own choosing.

None of these are individually complicated. Most of them boil down to the same move: replace a proof obligation Z3 would have to grind through with arithmetic reasoning, with one it can close by equality reasoning instead. But a formula that still hits several of the harder cases un-simplified can be the difference between a few seconds and a timeout.

Results: Keccak and Reth

We ran the verifier over two real workloads:

• Keccak precompile: 61 hot basic blocks identified by powdr's autoprecompile selection, each optimized through roughly 40 pass-to-pass steps, for 2,451 equivalence checks in total.
• Reth block execution: a trace taken from the Reth Ethereum execution client, with 100 hot basic blocks, for 4,176 equivalence checks in total.

In both cases, the overwhelming majority of every optimization step across every hot block was proved equivalent automatically. We found no counterexamples on either of these two workloads at their current state: every non-timeout outcome was a proof of equivalence, not a refutation.

The remaining fraction are solver timeouts: inconclusive, not disproofs. They aren't evenly spread across passes, either. For Keccak, 80% of them (20 of 25) come from a single basic block that is an order of magnitude larger, by circuit size, than any other block we optimized. It's one oversized outlier, not evidence that some particular pass is systematically hard. Reth has no single outlier like that. Its 53 timeouts are spread across 27 of its 100 blocks, and no single pass dominates either (the worst, an internal-solver step, accounts for only 11). But it's the same underlying story played out over a longer tail instead of one spike. Blocks with at least one timeout are, on average, about 9x larger (by circuit size) than blocks with none. And 18 of Reth's 30 largest blocks have a timeout somewhere in their pass chain.

Solve time tracks circuit size closely in both workloads (note the log/log scale). Keccak's timeouts (orange) are dominated by one oversized block; Reth's are spread across a longer tail of medium-to-large blocks instead.

It's worth putting these numbers in context. They're the product of about six weeks of tuning both powdr's optimizer and our own encoding, not a one-shot result. The very first end-to-end runs against these same 2,451 and 4,176 checks were back in late June. They only closed 76.5% of the Keccak checks and 81.9% of the Reth checks automatically, at an average of 34s and 65s per check respectively.

Over successive iterations, we made three kinds of changes. We made the formula easier to close via cheap equality reasoning instead of expensive arithmetic proofs. We added targeted special-purpose reasoning over the memory bus. And we did a wholesale reimplementation of our formula-rewriting layer in Rust. (The core encoding and pre-analysis are still in Python, but the rewriting step, which does the bulk of the simplification work, got a large speed-up from the rewrite.) That climbed to today's 99.0% / 98.7%. The average check now takes under 7 and 8 seconds respectively, roughly a 5–8.5x drop in per-check solving time. The fraction fully proved jumped by 17 to 22 points.

Along the way, the verifier also surfaced a handful of minor issues in powdr's optimizer. Most were cosmetic inconsistencies in how intermediate results were represented. One was a genuine correctness edge case in how timestamp overflow was handled, found early on in a small test program. It wasn't exploitable, and the powdr team had already acknowledged and accepted it. That's exactly the kind of thing an independent equivalence check is supposed to catch.

Running the full check for a workload, using 28 parallel workers, took about 12 minutes for Keccak and 23 minutes for Reth. Summed sequentially, the underlying solver work comes to roughly 5.4 CPU-hours for Keccak and 10.5 CPU-hours for Reth. That gives a sense of how much automatic, per-pass verification the pipeline buys back, for a per-workload cost measured in minutes, not days.

Conclusion

We set out to answer a fairly narrow question: can powdr's autoprecompile optimizations be checked for correctness, independently and automatically, at real production scale? The answer is yes.

Across two real-world workloads and 6,627 combined pass-to-pass equivalence checks, the approach held up. We built a precise soundness/completeness definition of equivalence, an SMT encoding on an off-the-shelf solver, and a verifier that proved the overwhelming majority of those checks automatically. The small remaining fraction were inconclusive timeouts, not open questions about correctness. Six weeks of tuning took the very first end-to-end runs from 77–82% automatic to over 98%. Along the way, the verifier did exactly what an independent check is for: it caught a handful of real, if minor, issues in the optimizer itself.