Formal Verification

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

• Field kernels explains the HOL Light proof method and the scalar Fp128 proofs.
• Scalar Fp64 proofs explains the first verified Prime64Offset59 slice and the limits of its connection to production Rust.
• Z3 verifier