Least Authority has been awarded a grant from the Ethereum Foundation’s Verified zkEVM program to create a comprehensive Lean blueprint for two cryptographic protocols, STIR [ACF+25] and WHIR [ACF+24], which are interactive oracle proofs of proximity (IOPPs) for Reed-Solomon codes. The zkEVM Program is a recent initiative that aims to provide a safer and more robust foundation for the future of decentralized applications. Formal Verification has seen significant advancement in recent years, especially within the realm of Ethereum and zero-knowledge proofs.
The long-term goal of our project is to formally verify the STIR and WHIR protocols in Lean. In this grant, we aim to focus on a Lean blueprint of both protocols, as the first step in that process. The key task is to lay out the list of theorems, lemmas, and definitions necessary to prove completeness and soundness for STIR and WHIR, expressed as Lean statements and visualized as Lean blueprints.
Formal verification is a suite of mathematical techniques used to prove or disprove the correctness of a system’s design relative to a formal specification. Unlike traditional testing, which can show the presence of bugs (rather than their absence), formal methods seek to verify system properties exhaustively. When well-executed, formal verification can provide an extremely high level of certainty about correctness in specific areas.
In the case of ZK applications, formal verification can help ensure:
- Security of protocol implementations: It offers assurance that a protocol’s design holds under all possible inputs and states and adheres to the required security properties.
- Quality of cryptographic primitives: It gives confidence that cryptographic components, such as zero-knowledge proof circuits, function consistently and resist known attack vectors.
Zero-knowledge Virtual Machines (zkVMs) integrate zk-proofs into the Ethereum Virtual Machine (EVM) environment, enabling developers to run privacy-preserving and/or scalable computations while maintaining trustlessness and compatibility with the broader Ethereum network.
However, zkVMs add a layer of complexity, particularly in the following areas:
- Circuit Design: Building circuits that accurately capture the semantics of a RISC-V execution can be error-prone.
- Security of Proof Generation: Mistakes in zero-knowledge proof generation or verification could render the system insecure.
- Performance Constraints: The complexity of circuit computations must be balanced with on-chain transaction costs and real-time user experience.
Given these challenges, formal verification is particularly advantageous. Mathematical proof that a zkVM’s design and implementation satisfy certain properties, such as correctness of state transitions or immutability of data, reduces the risk of bugs making it into production.
At Least Authority, we’re committed to guiding projects through the dynamic space of cryptographic security and decentralized protocols. If you’re curious about how we can help with formal verification for your protocol or want to learn more about auditing zero-knowledge systems, reach out to us. We’re here to help you build and verify robust, privacy-focused solutions that align with the highest standards in security research and blockchain engineering.