Etheorem: Formell verifizierte Konsens-Spezifikation für Ethereum
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 undWeiterlesen
