@verityclient

The Provable Consensus Client — a formally verified @leanEthereum client built with @leanprover

verityclient.com/
Joined April 2026
  • Tweets36
  • Following9
  • Followers132
11Media
The strawmap has been updated! - Shorter slots and PQ upgrades move to earlier forks - leanVM frames added to the EL roadmap - Uncertainty marker removed from “leanCL STF in Lean 4” @leanEthereum strawmap.org/
1
4
11
283
⚠ the calendar timeline has also shifted later, so this does not necessarily mean earlier delivery ↓ previous version
17
We get step to next stage 🧙 to prove the correspondence of spec and implementation with Aeneas github.com/NyxFoundation/ver…

GitHub - NyxFoundation/verity-aeneas-proofs: Aeneas-generated Lean semantics and correspondence...

Aeneas-generated Lean semantics and correspondence proofs for Verity against formal-leanSpec - NyxFoundation/verity-aeneas-proofs

github.com
1
1
2
732
For examaple, We are prototyping Option 4 inspired by evm-asm✨ github.com/NyxFoundation/cl-…

GitHub - NyxFoundation/cl-asm: Experimental design for a Lean 4-verified RISC-V consensus-layer STF...

Experimental design for a Lean 4-verified RISC-V consensus-layer STF prototype - NyxFoundation/cl-asm

github.com
Verity@verityclientSep 26
Replying to @verityclient
@verityclient is currently using Option 2, but with the discovery of several alternative approaches, it is considering a change in architecture.
1
129
“Formally verified client” doesn’t automatically mean the binary users run is verified. This article explores where proofs end, what remains in the TCB, and five paths toward E2E verification ethresear.ch/t/ethereums-tcb…

Ethereum's TCB, Part 1: The client

by George and Kev. Thanks to Alex Hicks for the many stimulating discussions that shaped this post. Motivation It’s 2026 and AI has been breaking the Internet lately. Formal verification (FV) seems...

ethresear.ch
1
1
1
2
780
@verityclient is currently using Option 2, but with the discovery of several alternative approaches, it is considering a change in architecture.
1
1
166
We experimentally integrated this into Verity through a C ABI github.com/NyxFoundation/ver…

feat: evaluate Lean SSZ hash tree roots by adust09 · Pull Request #41 · NyxFoundation/verity

Summary vendor the Lean 4 SSZ implementation from Add a Lean second implementation, proved and checked against this one ethereum/ssz-specs#132 at commit 463a311d61353cc83de04e1c7d71834b9f354784 ad...

github.com
Thomas Coratger@tcoratgerSep 15
We just merged Lean4 implementation of SSZ! Still a huge amount to iterate on, especially making the Astra-generated proofs more human-readable. But Lean/Python cross-testing in CI has already caught a few subtle bugs in the Python spec :) github.com/ethereum/ssz-spec…

Add a Lean second implementation, proved and checked against this one by tcoratger · Pull Request...

A second implementation of SSZ, in Lean 4, that this one is checked against. Why a second one A reference implementation is only as right as its tests. Two independent implementations disagree loud...

github.com
1
2
6
1,556
1/10 Do you know Decoupled Consensus? It resolves multiple problems long faced by @ethereum ’s consensus algorithm. We are formally verifying it in @leanprover ethresear.ch/t/unblocking-fa…

Unblocking faster finality with decoupled consensus

Thanks to the EF Consensus team for discussion and comments In the current consensus protocol, the timelines of block production and finality are coupled. A large committee (consisting of 1/32 of the...

ethresear.ch
1
3
1
14
3,809
more replies
9/10 Minimmit builds on Simplex and reduces communication rounds and messaging under realistic network conditions. github.com/NyxFoundation/min…

GitHub - NyxFoundation/minimmit-fv: Formal-verification reference notes for the Minimmit consensus...

Formal-verification reference notes for the Minimmit consensus protocol (arXiv:2508.10862, FC'26) - NyxFoundation/minimmit-fv

github.com
1
1
4
1,222
10/10 These formalizationsare under review by the　@ethereumfndn FV team. We contribute to core protocol. Check the repos above for the next generation of Ethereum consensus. Feedback welcome!
5
98
While formalizing the @leanEthereum spec in @leanprover, we found several critical bugs hiding in the spec itself. Here's what we found 🧵 github.com/NyxFoundation/for…

GitHub - NyxFoundation/formal-leanSpec

Contribute to NyxFoundation/formal-leanSpec development by creating an account on GitHub.

github.com
4
12
1
57
20,925
more replies
Closing Formal verification prevented many problems before they could do harm. These were serious issues that had gone unnoticed until now — and testing had missed every one of them.
1
4
418
We'll keep bringing the safety of formal verification to Ethereum. github.com/NyxFoundation/ver…

GitHub - NyxFoundation/verity: The Provable Consensus Client — a formally verified Ethereum...

The Provable Consensus Client — a formally verified Ethereum consensus client built with Lean 4. - NyxFoundation/verity

github.com
5
377
Load more