lean Ethereum Part 6: Formal Verification with Alex Hicks

Anna Rose introduces the podcast "Zero Knowledge," where Nico interviews Alex Hicks from the Ethereum Foundation, concluding the Lean Ethereum mini-series. They discuss formal verification within the Lean Ethereum vision and the ecosystem's efforts to achieve machine-checked guarantees across the ZK stack, including RISC-V, ZKVM, Circuits and Constraints systems, compilers, and cryptographic primitives.

Alex Hicks shares his background, detailing his transition from physics and mathematics to computer science due to concerns about academic job prospects and a growing interest in privacy and security. His research focused on transparency-enhancing technologies, particularly using blockchain as a transparency log. The conversation emphasizes the importance of formal verification, defined as producing machine-checkable proofs of statements, and distinguishes between theorem solvers and proof assistants. Proof assistants like Lean, Coq, and Isabelle require manual proof writing and vary in their logical foundations and soundness guarantees.

Trust in code is paramount, especially in large codebases. If a proof is false, it signals an inconsistency, highlighting the importance of verifying the kernel's consistency through tools like Lean and Metacop. Client diversity is crucial, as different implementations of the Lean kernel exist in languages like Lean, C++, and Rust. Running proofs across these implementations can enhance assurance, provided the logical foundations are sound.

Formal verification of code involves creating theorems that resemble traditional mathematical statements, with proofs structured in a readable manner despite complex notation. The process in the Lean environment allows for maintaining, debugging, and optimizing proofs, which can lead to more general proofs that enhance automation and component reuse. Specifications are critical; an incorrect specification can render proofs unreliable, particularly in cryptographic code where properties like constant time execution must be proven.

Extracting code from languages lacking formal semantics into a proof assistant like Lean requires careful translation. The conversation emphasizes the need for knowledgeable individuals to analyze behavior across languages, particularly in Rust, where purely functional code is easier to reason about than imperative code with side effects. Tools like InEOS and Hacks facilitate the translation of Rust code into Lean, but high assurance is preferred over formal verification, indicating a trust level based on testing rather than proof.

The discussion references CompSat, a formally verified C compiler, noting the extensive effort involved in its verification. While compiler passes may be verified, the front end often is not, raising questions about trust in compiler specifications and the implications of compiler optimizations on code behavior. The conversation highlights the complexities of verifying Rust code in Lean, emphasizing the need for robust engineering practices due to the evolving nature of both compilers.

The focus is on transitioning to formal verification of the Lean Ethereum stack, particularly the RISC-V CKBMs. The team is working on parallel coverage of different stack components, especially the execution layer. A Lean backend has been developed from the official RISC-V specification written in SAIL, allowing for the integration of future specifications and ensuring that the backend is part of the trusted boundary.

Clarifications are made regarding the RISC-V specification and its implementation, with the RISC-V Foundation defining the official spec and teams in Cambridge and SAIL handling the implementation. The backend effectively maps SAIL to Lean, sharing similar logic. Constraints for ZKVM RISC-V sockets are verified against the RISC-V spec, with the mapping of constraints into Lean being facilitated through the AST from the source language.

The conversation also addresses the verification of constraints and the optimization of witness generation by CKVM teams to prevent performance bottlenecks. Writing constraints in Lean using DSLs like Clean or ZK Lean is proposed as a way to significantly improve proof quality. Examples illustrate the efficiency of soundness and completeness proofs in Clean, while challenges arise with larger files, which can crash development tools.

The conversation emphasizes the critical need for maintaining code in repositories, particularly the importance of keeping dependencies updated to prevent breaking changes. Regular updates to software proofs are necessary, typically taking 30 minutes to an hour each month. Soundness issues can arise when code is verified against specific commit hashes, and failing to reproof after code changes can lead to significant concerns.

The discussion transitions to the role of AI and large language models in proof systems, highlighting AI's capability to generate extensive outputs that assist in proof verification. The need for formally verified specifications for the fry protocol is underscored, focusing on creating executable code rather than abstract functions. The successful development of the fry specification and the use of AI tools for proving complex theorems are highlighted, along with the implementation of a script to identify missing proofs in the library.

The conversation reflects on initial skepticism regarding the use of proof assistants like Lean in cryptography, noting the challenges in convincing cryptographers to adopt this approach. The potential for Lean and similar tools to be integrated into research and software development processes is emphasized, suggesting that researchers document protocol specifications in ArcLib to enable automated proofs and expedite peer review.

The conversation highlights the necessity of optimization passes in compilers, specifically mentioning Montgomery and Barrett reductions. Alex Hicks emphasizes that not all LLVM IR optimizations are essential. He discusses the importance of compilers in proof systems that operate on CPUs without dependence on GPUs. Future plans include compiling from ARCLIP specifications to hardware backends with a compiler developed in Lean, aiming for performance enhancements over Rust. The overarching goal is to provide assurance for the entire Lean stack by reducing boundaries.