Ethereum betreibt ein Multi-Client-Modell, in dem mehrere unabhängige Implementierungen (Lighthouse, Prysm, Teku, Lodestar, Grandine) dieselbe Konsens-Logik ausführen. Historisch führten unterschiedliche Interpretationen der Python-Referenz-Spezifikation (pyspec) zu gefährlichen Chain-Splits. Das Projekt Etheorem liefert eine in Lean 4 geschriebene, ausführbare und mathematisch formell verifizierte Konsens-Spezifikation für die Forks Fulu, Gloas und Heze. Durch maschinell geprüfte Beweise ersetzt es informelle Dokumentation und reine Testvektoren und bietet damit mathematische Garantien für die Ethereum-Netzwerk-Resilienz.

Formale Verifikation der Ethereum-Konsens-Spezifikation

Etheorem besteht alle pyspec-Testvektoren für Statusübergänge, Fork-Choice und SSZ-Container für die drei Forks. Die Tests basieren auf den consensus-spec-tests Version v1.7.0-alpha.11 und decken sowohl das mainnet als auch die minimal Presets ab – insgesamt 2 Referenz-Presets.

Abgedeckte Testfälle

• 2215 bestandene SSZ-Generic-Testfälle (Wire-Format) aus v1.7.0-alpha.13 (2026)

Trennung von Ausführung und Beweis: ‚fast‘ vs. ‚pure‘

Das Framework unterscheidet zwei Konfigurationen:

• fast: Nutzt optimierte C-Bibliotheken via FFI (z. B. blst für BLS-Signaturen, native SHA-256) für schnelle Konformitätstests gegen offizielle Vektoren.
• pure: Verwendet reine Lean-Definitionen und symbolische Kryptografie. Hier werden Beweise ausschließlich auf den drei Lean-Kernel-Axiomen propext, Classical.choice und Quot.sound aufgebaut. Keine externen Kryptobibliotheken gehören zur Trusted Computing Base.

SSZ-Bibliothek SizzLean: Maschinell geprüfte Korrektheit

Die integrierte SSZ-Bibliothek SizzLean liefert für alle Typen der Konsensschicht maschinell geprüfte Korrektheitsbeweise:

• Round-trip (Serialisierung ↔ Deserialisierung)
• Non-malleability (Manipulationssicherheit)
• Size-bound (Längenbeschränkung)

Damit wird das gesamte SSZ-Layer-Verhalten formal abgesichert.

Aktueller Stand: Funktionen, Testfälle und Beweisabdeckung

Über die drei Forks hinweg umfasst die Spezifikation 585 Funktionen. Davon sind bislang:

• 8 Konsens-Funktionen vollständig formal charakterisiert.
• 29 weitere Funktionen in Theoremen eingebunden.

Die aktuelle Beweisabdeckung ist damit ein Anfang, aber noch nicht lückenlos. Das Projekt führt ein Proof-Ledger, das den Fortschritt transparent macht.

Bedeutung für die Multi-Client-Resilienz von Ethereum

Ethereum unterscheidet sich von den meisten Blockchains durch mehrere unabhängige Konsens-Clients. Divergierende Interpretationen der Python-Referenz haben historisch das Risiko von Netzwerkspaltungen geschaffen (Foresight News 2026). Etheorem liefert eine eindeutige mathematische Semantik, die allen Clients eine einheitliche Referenz bietet und damit das Risiko von Chain-Splits reduziert.

Verifikation zukünftiger Protokoll-Upgrades (ePBS, FOCIL)

Etheorem modelliert nicht nur den aktuellen Stand, sondern auch geplante Upgrades:

• Gloas integriert die Enshrined Proposer-Builder Separation (ePBS / EIP-7732) und fügt 109 neue Spezifikations-Funktionen hinzu (gegenüber der Fulu-Basis von 158 Funktionen).
• Heze adressiert Zensurresistenz durch Fork-Choice Inclusion Lists (FOCIL / EIP-7805) und erweitert Gloas um weitere 12 Funktionen.

Durch die formale Modellierung dieser Upgrades können Unschärfen bereits im Entwurfsstadium entdeckt werden.

Minimierung der Trusted Computing Base

In der pure -Konfiguration werden BLS-Signaturen symbolisch behandelt, während das Hashing über eine rein in Lean implementierte SHA-256 (FIPS-180-4 konform) erfolgt. Damit beruht die gesamte Beweisführung ausschließlich auf den drei genannten Kernel-Axiomen und schließt kryptografische Implementierungen aus der Vertrauensbasis aus.

Kritische Betrachtungen und offene Herausforderungen

• Diskrepanz zwischen Spezifikations-Verifikation und Client-Produktionscode: Etheorem verifiziert die mathematische Spezifikation, aber produktive Clients (Rust, Go, Java usw.) können weiterhin Implementierungsfehler enthalten, solange keine formalen Übersetzungs- oder Verifikationsbrücken in die Client-Codebasen führen.
• Geringe Beweisabdeckung in frühen Projektphasen: Mit nur 8 von 585 Funktionen vollständig charakterisiert bleibt ein erheblicher manueller und KI-gestützter Beweisaufwand nötig, um die gesamte Konsens-Logik formal zu verifizieren.

Häufig gestellte Fragen (FAQ)

Warum reicht die bisherige Python-Referenzspezifikation (pyspec) nicht aus?Python-Code ist ausführbar und dient als Testvektor-Vorlage, erlaubt jedoch keine mathematisch rigorosen Korrektheitsbeweise. Mehrdeutigkeiten, dynamische Typisierung und implizite Zustands-Mutationen können unbemerkt bleiben und zu abweichenden Implementierungen führen.Was bedeutet die Trennung in ‚fast‘- und ‚pure‘-Konfigurationen in Etheorem?Die ‚fast‘-Konfiguration nutzt optimierte C-Bibliotheken via FFI für performante Tests. Die ‚pure‘-Konfiguration verwendet reine Lean-Definitionen und symbolische Kryptografie, sodass der Lean-Kernel die Theoreme ohne externe Abhängigkeiten prüfen kann.Können Staker oder Validatoren Etheorem direkt als Node-Software betreiben?Nein. Etheorem ist als formale, verifizierbare Referenzspezifikation konzipiert, nicht als hochoptimierter Produktions-Client mit P2P-Netzwerkschicht, Datenbank-Tuning und Hardware-Parallelisierung.

Fazit

Etheorem stellt einen bedeutenden Schritt hin zu einer mathematisch gesicherten Ethereum-Konsens-Spezifikation dar. Durch die Trennung von Ausführung und Beweis, die minimale Trusted Computing Base und die formale SSZ-Bibliothek wird ein hohes Maß an Sicherheit erreicht. Die bisherige Test- und Beweisabdeckung belegt bereits die Machbarkeit, während die geplanten Upgrades Gloas und Heze die zukünftige Skalier- und Zensur-Resistenz unterstützen. Trotz offener Herausforderungen – insbesondere der noch niedrigen Beweisabdeckung und der Notwendigkeit, die formale Spezifikation in produktive Clients zu überführen – liefert Etheorem ein solides Fundament, das das Risiko von Konsens-Divergenzen im Ethereum-Ökosystem nachhaltig reduziert.