Orientation

Approach	What is proved	Where the dominant cost comes from
zkVMs (RISC Zero, SP1)	The execution of a machine running a program	Arithmetising the machine: every step of an instruction-set interpreter enters the witness
Circuit languages (Circom and kin)	A hand-authored constraint system	Authoring: the rule must be manually re-expressed as circuits, per application
Mina	Validity of a succinct chain, per its recursive design	Proving inside an account model: state lookups sit on the critical path of every transition
Modulus	Satisfaction of a first-order predicate over a transition	The statement itself: connectives translate directly to polynomial operations