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
Most verification frameworks are tied to one arithmetization: Picus and Ecne to R1CS, Halva to PLONKish, CertiPlonk to Plonky3 AIRs, StarkWare's proofs to the Cairo AIR. Clean is the exception and targets all of them (AIR, PLONK and R1CS). 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).