Random Walks

Jolt-Qed

These are working notes about ongoing efforts to formally verify the jolt zkVm using the Lean proof assistant.

  1. Formally Verifying Jolt (Incomplete)
  2. How to Model a CPU in Lean
  3. Equivalence Statements And Assumptions
  4. Jolt System Mismatch
  5. Bug Report: DIVW Inline Sequence Incompleteness
  6. Automatic Bytecode Expansion Extraction