TL;DR
StarkWare uses a proof assistant called Lean to conduct formal verification – a process of proving that a system (software or hardware) meets a specific set of requirements using mathematical logic – to ensure that its tech performs exactly as intended. This labor intensive effort guarantees the correctness of the translation between computer programs and the polynomial equations used in blockchain scaling technology, setting StarkWare apart from its competitors.
What is Lean?
Lean is a programming language and an interactive proof assistant, a software tool that aids the development of formal proofs via human-machine collaboration. Lean allows complex mathematical proofs to be broken down into smaller, verifiable components in order to ensure the correctness of the system.
One can compare the difference between standard coding and coding supported by formal verification to the difference between a spell checker and a “truth checker” in word processing. A simple spell check ensures that there are no typos in the text. A “truth checker,” on the other hand, would also check if the statement you are making is actually true. For example, if you stated, “The Empire State Building was once the tallest building in the world,” the proving system would demand that you provide evidence for that claim before allowing you to save it.
As systems become more complex and modular, they become too dense for even the smartest human auditors to catch every edge case. Lean allows you to type mathematical statements into a computer and obtain mathematical certainty of the logical correctness of that proof. With Lean, every property is documented in code and every logical step is machine-checked. If a change breaks a proof, Lean identifies exactly what is broken and what needs to be fixed.
Note that formal proofs should not be confused with computational proofs, which are verified with very high probability. In the context of zero-knowledge (ZK) proofs, for example, a very weak verifier with minimal computational power can verify with high probability what the prover set out to prove.
How StarkWare Uses Formal Verification
StarkWare’s Lean project began several years ago and is a collaboration between StarkWare employees and several outside advisors: Professor Jeremy Avigad, director of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University; and Dr. Yoav Seginer, an independent consultant with a PhD in natural language processing and extensive experience in software development. By working with Jeremy and Yoav, StarkWare is bridging the gap between cutting-edge computer science and production-grade blockchain tech. While some blockchain projects use formal verification, most use automated tools like SMT solvers (which are faster to use but have “blind spots”) or symbolic execution. StarkWare’s approach with Lean is distinct:
- StarkWare uses Lean as the proof assistant. Because the logic is too complex for a “one-click” automated scanner, a human must manually explain the logic to Lean.
- Lean acts as the “source of truth.” It checks every logical step provided by the human and, once approved, formal verification is achieved.
- While simple formal verification, such as static analysis, can locate common bugs, to obtain an advanced level of soundness, the extreme precision of a proof assistant is required.
Project Highlights
Stone Prover
StarkWare’s first major Lean project focused on the Stone Prover. We used Lean to prove the mathematical translation between the Cairo Virtual Machine (VM) and the polynomial equations that encode it.
- The goal of this project was to prove that if you can solve the equations, it is (mathematically) guaranteed that the code has run correctly. We used Lean to ensure that no equation was missing from the translation.
- Lean successfully verified the proof, and no issues were found.
CairoZero
This project examined the soundness of CairoZero code.
- The purpose of this project was to prove the soundness of several important CairoZero functions. For example, proving that if the CairoZero code for signature verification runs successfully, it indeed means that the user signed the transaction.
- Lean verified the logic of signature verification within the CairoZero environment, bridging the gap between high-level user intent and low-level cryptographic proofs. In the process, Lean uncovered a small bug in the code, which the StarkWare team then fixed, along with completing the proof of the fixed code.
Cairo
This project focused on proving the soundness and completeness of the building blocks of the Cairo compiler, known as Sierra’s libfuncs.
- The goal was to prove that if the specs of a libfunc hold, then the compiled code will run successfully, and vice versa; if the compiled code runs successfully, the implication is that the libfunc guarantees hold.
- The result was that Lean proved many of the libfuncs used in Cairo compilation. In addition, Lean uncovered small bugs in some of the libfuncs, which the StarkWare engineering team then fixed.
S-two (Ongoing)
This ongoing project is similar to the Stone project, but this time we’re targeting S-two, our next-generation prover, which is built on a much more efficient architecture.
- The purpose is to verify S-two’s modular components to ensure they are consistent with the same Cairo specifications used by Stone.
- StarkWare is working on proving S-two’s core opcodes, the basic instructions of the VM. This work is ongoing, but nearing completion.
Privacy
Unlike previous projects, Lean is being used alongside our engineering efforts on privacy, treating formal proofs not as a final step, but as a compass. Rather than coding and then checking for issues, certain privacy and compliance features, including traceability, double-spend prevention, and what information to reveal in Starknet events (the public logs of transaction activity), have been implemented only after they have been mathematically validated in Lean. This approach ensures that the foundation of our developing privacy layer is secure from the first line of code.
Learn More
StarkWare’s work with Lean has evolved into a core part of our engineering DNA. By choosing the “hard road” of Lean, we provide a level of certainty that standard audits simply cannot match.
If you’re interested in a deep dive into StarkWare’s work with Lean, check out the whitepapers:
- A Proof-Producing Compiler for Blockchain Applications
- A verified algebraic representation of Cairo program execution
And keep an eye on the StarkWare website and the StarkWare and Starknet X handles to learn more about the tech that sets us apart.
