The Provable Consensus Client — a formally verified @leanEthereum client built with @leanprover
Joined April 2026
- Tweets36
- Following11
- Followers139
- Likes23
Verity retweeted
From our team, @adust09 will give a talk on the use of formal verification in client development at @eth_proofs call #9🏌
Verity retweeted
This theorem (left) means, the only way you can make proofs for two different things in the same position in the same Merkle tree, is by breaking the underlying hash function.
As a reviewer, you don't have to verify how Merkle branches are implemented or how the theorem is proven (right), you just have to verify what the theorem says, and that Lean verifies it.
And the beautiful thing is that you can even write live production code (including eg. CLI tools) directly in Lean.
