Formal Verification

This section describes the formal verification work and tools in Jolt.

Field kernels explains the HOL Light proofs for scalar Fp128 arithmetic and the limits of the current claim.
Z3 verifier