Jolt-Qed

This series describes the efforts to formally verify using the Lean proof assistant that the Jolt bytecode expansions faithfully represent their corresponding RISC-V instructions.