Jolt Formal Verification

This project is funded by Layer Zero Labs.

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.