sorryfreeLast reviewed 2026-09-13
Index › Glossary › Extraction (code to model)

Extraction (code to model)

Direct answerThe step that turns a deployed circuit or program into the object a prover reasons about, whether by instrumenting synthesis (Halva), compiling to an IR (LLZK), or translating source (hax, Aeneas).

In more detail

Extraction is part of the trusted computing base unless the extractor is itself verified. Frameworks that avoid it (Clean, where the Lean circuit is the source; CIVER, which runs inside the compiler) trade it for a code-generation or correspondence step instead.

Frameworks that address it

Halva, hax, Aeneas, LLZK.

Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Refinement, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Witness generation vs constraints

Getting help

Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt