What is Extraction (code to model)? Definition and why it matters
=================================================================

The 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).

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.

Source page: https://sorryfree.com/glossary/extraction/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13