Jolt QED: Formally Verifying Jolt Bytecode Expansion In Lean

This paper is currently in preparation, but I’d be happy to answer questions in the meantime. See A16z summer series for a brief talk about the work given by Quang Dao. A longer pre-recorded youtube talk will be available along with the eprint by the end of August.

A less formal but equally detailed blog series about the work can be found here