sorryfreeLast reviewed 2026-09-13
Index › Glossary › Arithmetization (R1CS, PLONKish, AIR)

Arithmetization (R1CS, PLONKish, AIR)

Direct answerThe 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.

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

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