Paper 2026/2157
Jolt-QED: Formally Verifying Bytecode Expansions In Lean
, University of Warwick, Layer Zero LabsAbstract
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.
- Keywords
- formal-verificationleansnarksjolt
- Contact author(s)
-
tcs @ randomwalks xyz
qvd @ andrew cmu edu
daniel_144 @ toastertime net
justin r thaler @ gmail com - History
- 2026-09-25: revised
- 2026-09-22: received
- See all versions
- Short URL
- https://ia.cr/2026/2157
- License
-
CC BY
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}
}
