Paper 2026/2157 Original: eprint.iacr.org/2026/2157 ↗
Jolt-QED: Formally Verifying Bytecode Expansions In Lean
Abstract
In this work, we verify, using the Lean 4 proof assistant, that the Jolt zk-VM's expanded programs faithfully emulate a RISC-V CPU. Prior work translated the official Sail specification of RISC-V into Lean. We extend this model to define the Jolt ISA in Lean. We build a generator that runs Jolt's Rust bytecode expander and renders its output as Lean programs. Finally, for 51 out of 58 such programs, we prove these expansions are equivalent to their corresponding RISC-V instructions. This lays the groundwork for proving completeness and soundness of further stages of Jolt's proving pipeline.
Metadata
- Available format(s)
PDF- Category
- Applications
- Publication info
- Preprint.
- History
- 2026-10-02: last updated
- 2026-09-22: published
- Short URL
- https://ia.cr/2026/2157
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2026/2157,
author = {Ari Biswas and Quang Dao and Daniel Ross and Justin Thaler},
title = {Jolt-QED: Formally Verifying Bytecode Expansions In Lean},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/2157},
year = {2026},
url = {https://eprint.iacr.org/2026/2157}
}