Spain: Succinct Proofs for Numerical Computations
Talkat 20th USENIX Symposium on Operating Systems Design and Implementation (OSDI '26) · 2026-07-13..07-15·
summary
Spain introduces approximate constraints and a new proof protocol that represents numerical operations directly over rationals with bounded error, instead of blowing them into exact finite-field equations. Implementation consists of three front ends, one back end producing prover and verifier binaries. Evaluation shows constraint counts drop by one to three orders of magnitude and proving time falls similarly for large workloads, yielding multiple-orders-of-magnitude improvements over AUDI and ZKLP and a working system for outsourcing numerical computations.
AI-written summary · about
chapters (12)
- 0:00Succinct proofs introduction
- 1:22Succinct proofs gap in numerical
- 2:46Constraint representation explosion
- 4:52Existing proof systems handling
- 6:38New front end for numerical proofs
- 8:03Approximate rational arithmetic
- 9:28Decomposing complex operations
- 10:53Front end and back end details
- 11:56Spain versus existing systems
- 13:19Alternative approaches
- 14:42Future directions and challenges
- 15:04Summary and applications
