Der Ethereum-Mitbegründer Vitalik Buterin schlug eine neue Programmiersprache vor. Sie würde direkt in Lean oder HOL, einen anderen formalen Beweisassistenten, kompiliert werden.
Die Idee zielt auf eine spezifische Lücke in der Art und Weise, wie Menschen die Ausgaben von KI lesen. Künstliche Intelligenz produziert zunehmend große Blöcke automatisierter Beweise, oft schneller, als es ein menschliches Team von Hand schreiben könnte. Nur wenige Leser können schnell bestätigen, was diese Beweise tatsächlich belegen.
Eine Sprache, die nur für KI-Beweisleser entwickelt wurde
Lean ist ein Beweisassistent, eine Software, die Mathematiker und Ingenieure verwenden, um Beweise zu schreiben, die ein Computer zeilenweise überprüfen kann. Ethereum-Forscher verwenden ihn bereits, um kryptografischen Code und Konsenslogik zu verifizieren. Beweisassistenten gibt es seit fast 60 Jahren, doch das Feld bleibt eine Nischenbeschäftigung.
In seinem Beitrag argumentierte Buterin, dass die internen Schritte eines Beweises nur eine Anforderung haben. Diese Anforderung ist mathematische Korrektheit, nicht mehr. Leser inspizieren diese Mechanismen nie direkt. Definitionen und Theoreme funktionieren anders, da Menschen diese Teile lesen, um zu lernen, was ein Stück Software tatsächlich garantiert.
Buterin erkundete eine verwandte Trennung in einem Blogbeitrag im Mai. Dort zeigt ein mathematischer Beweis, dass effizienter Low-Level-Code mit einer separaten, lesbaren Spezifikation übereinstimmt, sodass eine einzige Prüfung beide Versionen gleichzeitig abdeckt.
Seine Zeitplanung stimmt auch mit Ethereums eigenem Wiederaufbauprojekt überein, das einen separaten Spitznamen trägt, den Lean Ethereum-Fahrplan. Forscher entwickeln unterdessen einen formal verifizierten ZK-EVM, eine null-wissen-beweisbare Version von Ethereums virtueller Maschine (EVM), unter Verwendung vergleichbarer Methoden.
KI schreibt die Beweise, Menschen überprüfen die Ansprüche
Große Sprachmodelle können bereits nutzbare Lean-Beweise schreiben. Buterin hat Claude und Deepseek 4 Pro als fähige Werkzeuge benannt, neben Leanstral, einem kleineren Modell, das speziell für Lean optimiert ist. Ein Beispielprojekt ist evm-asm, eine EVM-Implementierung, die gegen ein lesbares Referenzdokument verifiziert wurde. Diese Fähigkeit spiegelt die Denkfähigkeiten wider, die Entwickler in einer kürzlichen Buterin-KI-Herausforderung gezeigt haben. Tester haben diese Herausforderung innerhalb von Stunden gelöst.
Die Einsätze gehen jedoch über den Komfort hinaus. Sicherheitsforscher haben in diesem Jahr einen Anstieg von KI-unterstützten Exploit-Versuchen verfolgt. Formal verifizierter Code bietet eine Verteidigung gegen diesen Trend. Eine freundlichere Spezifikationssprache würde es Entwicklern ermöglichen, Ansprüche zu überprüfen, ohne sich durch den umgebenden Beweis zu wühlen.
Über Ethereums Forschungszirkel hinaus
Buterin testet diese Ideen weiterhin öffentlich, da er kürzlich ein anonymes Plakat demonstrierte, das mit null-wissen-Beweisen erstellt wurde. Die Demo zeigte, wie verifizierbare Ansprüche von Forschungsrepositorien in funktionierende Produkte überführt werden können. Forscher haben auch begonnen, Konsens-Clients in Lean formal zu verifizieren, um Fehler frühzeitig zu erkennen.
Dennoch spiegelt die Richtung ein vertrautes Muster wider: schnelles Code von lesbaren Ansprüchen trennen und dann beweisen, dass die beiden übereinstimmen.
Es gibt noch keinen Prototyp der neuen Sprache, und Buterin ließ die genaue Syntax offen. Entwickler könnten sich auf einen gemeinsamen Standard einigen oder sich stattdessen mit mehreren inkompatiblen Dialekten zufrieden geben. Diese Wahl könnte bestimmen, wie schnell AI-überprüfter Code in Produktionssysteme gelangt.
Quelle: BeInCrypto
