Jolt Formal Verification
This is an ongoing effort to formally verify the Jolt zkVm in Lean4. Currently, we are focused on verifying that the Jolt bytecode expansions do not alter guest program behaviour.
This is an ongoing effort to formally verify the Jolt zkVm in Lean4. Currently, we are focused on verifying that the Jolt bytecode expansions do not alter guest program behaviour.