Writing the cryptography spec in Lean 4, cryptographic rules checked by proof
Strawmap Hegotá (2027) · cryptography specs in Lean 4
The specification of the cryptography the consensus layer uses is written not as a prose document but as code in the proof assistant Lean 4. This lets a computer check the spec for errors.
Why it is needed
The Ethereum consensus layer runs on cryptography such as signatures and hashes. Until now, these rules have mostly been written up as English documents and Python reference code. That reads well for people, but whether the spec is free of contradictions and really satisfies its safety properties is only checked by eye. Different client teams may also read the same sentence differently and produce different results. Lean 4 is a proof assistant, in which a computer checks a mathematical proof line by line, and also a programming language. If the cryptography spec is written in Lean 4, the spec itself becomes runnable code, and a claim such as "this function always keeps this property" can come with a proof that a machine checks. This leaves less room for interpretation and allows a stricter comparison of whether an implementation deviates from the spec. As the placement of post-quantum key registration in the same column shows, the consensus layer is preparing to bring in new cryptography. A spec-level mistake when adding new cryptography becomes a safety problem for the whole network, so the aim is to write it from the start in a form a machine can verify. This item is work outside the protocol that does not directly change chain rules. The Hegotá column is the Strawmap's estimate, not a commitment.
How it works
- Write the spec as Lean 4 code Cryptographic rules such as signature verification and hash computation are defined as Lean 4 functions rather than sentences. Because the definition is itself runnable code, you can feed in inputs and see the results right away.
- Prove the properties that must hold A property such as "a correct signature always passes" is written as a theorem and given a proof. If the proof has a gap, Lean 4 will not accept it.
- Check implementations against the spec Client teams use this spec as the reference and check that each of their implementations produces the same result for the same input.