Research
What the claims rest on.
The translation from first-order logic into polynomials is published, reviewed work. It is also the reason Modulus has a different cost structure from a zkVM rather than a better version of the same one.
Arithmetisation of computation via polynomial semantics for first-order logic
Murdoch J. Gabbay, Heriot-Watt University. Also in the Journal of Applied Logics 12(6), October 2025.
A compositional translation from first-order logic into polynomials, connective by connective, with soundness and completeness treated directly. The validity of a formula becomes a checkable property of the polynomial it produces. There is still a compiler, and it does real work. What it does not do is force the computation into a shape chosen for something else. Each connective has a polynomial form it maps onto, so the constraints land where the logic already sits. A zkVM instead arithmetises the machine that runs your program, and every step of that interpreter enters the witness alongside your actual claim. Modulus has no machine to arithmetise, and that is what the measured gap is made of.
| In the logic | In the polynomial |
|---|---|
| Truth | zero |
| Falsity | a strictly positive value |
| Conjunction, universal quantification | addition |
| Disjunction, existential quantification | multiplication |
The soundness argument, the proving backend Modulus emits to, and the complete reference list, including the market and security figures cited elsewhere on this site, are in the documentation.