lean

Automatic Bytecode Expansion Extraction

Jolt System Mismatch

Formally Verifying Jolt (Incomplete)

Equivalence Statements And Assumptions

How to Model a CPU in Lean

Bug Report: DIVW Inline Sequence Incompleteness

Incompleteness in Jolt's DIVW inline sequence.