Succinct argument (SNARK)

A succinct non-interactive argument of knowledge lets an untrusted prover convince a verifier that a computation ran correctly, by sending a short certificate the verifier checks much faster than performing the computation itself flock.

Three properties do the work: the proof is short and cheap to check regardless of how long the computation was, and it is an argument rather than a proof — sound against a computationally bounded prover, up to a security parameter, with some tiny probability of accepting a false statement by design. flock targets 100 bits of soundness, meaning round-by-round error at most 2⁻¹⁰⁰.

Not theorem proving. ../research-wiki owns formal methods: deductive proof, machine-checked, Lean. That tradition's "proof" is a derivation valid by construction. This one's is a probabilistic argument about an execution, deliberately unsound with negligible probability. Both use the words prover and verifier. They are different subjects and this spoke never merges them on the vocabulary.

The shape of a modern construction

Most current systems follow one framework: compile a polynomial interactive oracle proof into an argument using a polynomial commitment scheme binius. Two families of commitment sit underneath:

• Elliptic-curve based — KZG and relatives, resting on discrete-log hardness in curve groups. Small proofs; groups must be ~256 bits, which makes the prover expensive.
• Hash and code based — FRI, Brakedown, Ligerito, resting on linear error-correcting codes and collision-resistant hashes. Larger proofs, much faster provers, and post-quantum as a side effect, since no group hardness is assumed. Both founding systems here are in this family.

The multilinear line (Spartan, HyperPlonk, CCS) bypasses polynomial multiplication using the classical sumcheck protocol, and is what lets a scheme work over tiny fields without embedding overhead binius. Both sources build on it.

The prover is the bottleneck, and recursion is the escape hatch

Proof size and verification time can usually be fixed after the fact by recursive composition: prove with a fast system that emits big proofs, then prove that verification with a slow system that emits small ones. What recursion cannot fix is prover time, which is why both founding papers spend their effort there and why concrete-efficiency is measured in proving throughput first.

The gap is large. General-purpose zkVM provers run four to six orders of magnitude slower than native execution flock. Restricting the problem is how that comes down: flock proves batches of one circuit and reaches ~250×, explicitly because batching removes the permutation and memory-checking arguments a general system must carry.

Arithmetization: what the circuit is written in

A statement must be expressed in a form a proof system can consume. R1CS (rank-1 constraint systems) and Plonkish are the two in the founding corpus, and the choice is a performance decision: flock picks R1CS over Plonkish because its witness is smaller — it does not commit to the outputs of addition gates. Whether the circuit is Boolean (AND/XOR over bits) or arithmetic over a large field is the other axis, and the one binary-fields is about.

Related

binius · flock · binary-fields · concrete-efficiency · indistinguishability-obfuscation · synthesis