Arithmetization (R1CS, PLONKish, AIR)
The encoding of a computation as polynomial constraints over a finite field: rank-1 constraint systems (Groth16, gnark), PLONKish gates with copy and lookup constraints (Halo2), or algebraic intermediate representations over execution traces (STARKs, Plonky3, SP1).
In more detail
Verification frameworks are tied to arithmetizations: Picus and Ecne to R1CS, Halva to PLONKish, Clean primarily to AIR with PLONK and R1CS support, StarkWare's proofs to the Cairo AIR. Check the framework page for the exact model before assuming coverage.
Related terms
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, Extraction (code to model), Witness generation vs constraints
Getting help
Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).