> For the complete documentation index, see [llms.txt](https://docs.moduluszk.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.moduluszk.io/soundness.md). # Soundness Evidence labels on this page: \[S] verified against a primary source; \[A] argued. Facts established by the project's own test suite are labelled confirmed by execution. ### What is being claimed The soundness claim of the system is narrow and precise: a proof accepted by the verifier establishes, at the stated security level, that a witness exists satisfying the named predicates over the stated transition. Everything on this page exists to say on what published grounds that claim rests, and by which mechanisms it is discharged in the shipped compiler. ### The semantics: one paper carries it The semantic foundation is eprint 2024/954, Arithmetisation of computation via polynomial semantics for first-order logic, Murdoch J. Gabbay, also published in the Journal of Applied Logics 12(6), October 2025. It is the only paper that supports a claim about zkFOL itself, and its contribution is a compositional, shallow translation from a first-order logic with equality directly into polynomials \[S]. Shallow and compositional carry the weight. The translation maps logical connectives directly to polynomial operations: truth to zero, falsity to a strictly positive value, conjunction and universal quantification to addition, disjunction and existential quantification to multiplication \[S]. Validity of a formula in a model becomes a checkable property of the resulting polynomial, to a high degree of certainty \[S]. The paper treats soundness and completeness of this semantics directly \[S]. The contrast with the prevailing route is the origin of the envelope this project measures. Existing systems arithmetise computation by encoding it into an abstract machine whose behaviour was arithmetised by hand, a deep embedding into a preconstructed artefact \[S, 2024/954's characterisation]. zkFOL has no machine in the middle: the predicate is translated as itself. That the removal of the machine is what the measured gap reflects is this project's argument \[A]; the measured gap itself is on the performance page. ### The mechanism actually shipped Two distinct arguments discharge integer reasoning in the shipped compiler, and each is presented only for its own mechanism. Where predicate arithmetic must be argued over the integers, the compiler uses a bit decomposition fold whose soundness rests on the backend's random-prime technique for integer arithmetic. Where a native lookup is used, a LogUp-style lookup argues over the prime field F\_q, and its soundness holds given that no wraparound occurs. The seam between those two regimes was the compiler's one known soundness gap. It is closed: a dedicated range-check pass, together with a fail-closed boundary guard that refuses rather than proceeds when the no-wraparound precondition cannot be established, is in place and under continuous test, with the full suite passing (confirmed by execution against the project's test suite). ### The backend zkFOL emits its polynomial claims to a hash-based proving backend in the Brakedown lineage. That layer is described in two third-party papers with no author overlap with zkFOL: Zinc (eprint 2025/316; Garreta, Waldner, Hristova and Dall'Ava; CRYPTO 2025), a hash-based succinct argument for integer arithmetic, and Zinc+ (eprint 2026/855; Nethermind Research and academic co-authors), which extends the approach to polynomial rings \[S]. Properties the backend inherits from that lineage, including transparency, in the sense of requiring no trusted setup, are those papers' claims about their own constructions \[S]. Those papers are cited in this documentation for one purpose only: describing what the backend layer is. Nothing on this page or elsewhere in this set uses their arguments or their benchmarks as evidence for zkFOL's performance, for its position against zkVMs, or for why its advantage exists. Claims of that kind are either measured in-house or grounded in eprint 2024/954. ### What a proof does not establish A proof establishes that the stated predicates hold over the stated transition. It does not establish that the predicates encode the right policy; reviewing the rule remains the author's work, and it is the only review left. It does not establish the truth of external inputs a predicate takes as given; a proof covers the application of a rule to inputs, never the provenance of those inputs. And it holds at the security level of the deployed verifier configuration, which is an operational responsibility, held to the same discipline as the mathematics.