> 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/comparison-models/against-zkvms.md).

# Against zkVMs

A zkVM proves that a machine correctly executed a program. The program is compiled for an instruction set, and the proof covers the interpreter's execution of it, so the witness carries the machine's steps rather than the author's statement. The vendors' product is compatibility: bring existing code, and the machine will be proved running it. That is a real product, and it defines the cost structure, because the arithmetisation of the machine is the layer being paid for \[A]. 

zkFOL has no machine to arithmetise. The published route translates first-order logic directly to polynomials, connective by connective, with no encoding into a preconstructed abstract machine \[S, eprint 2024/954]. The project's argument is that the measured gap is the removed layer, and that the gap is structural for the incumbents: a zkVM cannot delete the machine it emulates and remain a zkVM, so removing the layer is a change of product rather than an optimisation \[A]. 

The measured comparison is on the performance page and is public: like-for-like fib(10,000) by fast doubling on every system, on an AMD Ryzen 7 5700X under Linux against RISC Zero 3.0.5 and SP1 6.3.1, shows prove-time ratios from roughly 320x against RISC Zero's raw mode to roughly 4,900x against SP1's compressed mode, with memory ratios from roughly 30x to roughly 1,700x, reproducible from the public benchmark record \[S, benchmark record]. 

One boundary of the claim is stated here so nobody discovers it later. The advantage is a property of proving statements. A workload that consists of emulating a virtual machine in logic

would put the interpreter back into the witness and surrender the advantage \[A]. That is why Modulus enforces predicates and does not emulate anyone's execution layer.