Random Walks

Jolt-Qed

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

  1. Jolt: Introduction
  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
  7. Jolt Constraints