Ethereum-Mitgründer Vitalik Buterin hat eine neue Programmiersprache vorgeschlagen. Sie soll direkt nach Lean oder HOL kompiliert werden, das sind formale Proof-Assistenten.
Die Idee richtet sich an eine bestimmte Lücke beim Lesen von KI-Ausgaben. Künstliche Intelligenz erstellt immer häufiger große Blöcke mit automatisierten Beweisen, oft schneller, als es ein menschliches Team von Hand tun könnte. Jedoch können nur wenige Leser schnell überprüfen, was diese Beweise tatsächlich zeigen.
Eine Sprache nur für KI-Beweisprüfer
Lean ist ein Proof-Assistent, eine Software, die Mathematiker und Ingenieure nutzen, um Beweise zu schreiben, die ein Computer Schritt für Schritt prüft. Ethereum-Forscher verwenden ihn bereits, um kryptografischen Code und Konsenslogik zu prüfen. Proof-Assistenten gibt es seit fast 60 Jahren, jedoch ist dieses Feld weiterhin eine Nische.
In seinem Post erklärte Buterin, dass die einzelnen Schritte eines Beweises nur eine Anforderung erfüllen müssen. Diese Voraussetzung ist mathematische Korrektheit, mehr nicht. Leser schauen sich diese Abläufe nie direkt an. Definitionen und Theoreme sind hingegen anders, da Menschen sie lesen, um zu verstehen, was ein Softwareprogramm wirklich garantiert.
Buterin hat diese Trennung auch in einem Blogpost im Mai ausgeführt. Dort zeigt ein mathematischer Beweis, dass effizienter Low-Level-Code mit einer separaten, gut lesbaren Spezifikation übereinstimmt, sodass eine einzige Prüfung beide Versionen gleichzeitig abdeckt.
Sein Vorschlag fällt zudem mit Ethereums eigener Umstrukturierung zusammen, einer Initiative mit dem Spitznamen Lean Ethereum Roadmap. Forscher arbeiten gleichzeitig an einer formal geprüften ZK-EVM, das ist eine Version der Ethereum Virtual Machine (EVM), die den Nachweis per Zero-Knowledge-Proof erlaubt und ähnliche Methoden nutzt.
KI schreibt die Beweise, Menschen prüfen die Aussagen
Große Sprachmodelle können bereits brauchbare Lean-Beweise schreiben. Buterin hat Claude, Deepseek 4 Pro und auch Leanstral genannt, ein kleineres Modell, das speziell auf Lean ausgelegt ist. Ein Beispiel-Projekt ist evm-asm, eine geprüfte EVM-Implementierung anhand einer lesbaren Referenz. Diese Fähigkeit erinnert an die Argumentationskünste, die Entwickler bei einem aktuellen Buterin KI-Wettbewerb zeigten. Die Kandidaten lösten die Aufgabe innerhalb weniger Stunden.
Die Bedeutung geht jedoch über die reine Bequemlichkeit hinaus. Sicherheitsforscher haben in diesem Jahr einen Anstieg bei KI-gestützten Angriffsversuchen beobachtet. Formal geprüfter Code ist eine Verteidigung gegen diesen Trend. Eine benutzerfreundlichere Spezifikationssprache könnte es Entwicklern ermöglichen, die Aussagen zu prüfen, ohne sich durch den gesamten Beweis arbeiten zu müssen.
Jenseits der Forschung von Ethereum
Buterin testet diese Ideen weiterhin öffentlich, jüngst etwa mit einer anonymen Anzeigetafel, die mithilfe von Zero-Knowledge-Proofs realisiert wurde. Die Demo zeigte, wie überprüfbare Aussagen von der Forschung in fertige Produkte gelangen können. Auch beginnen Forscher, Konsens-Clients in Lean formal zu prüfen, um Fehler frühzeitig zu erkennen.
Dennoch zeigt sich hier ein bekanntes Muster: Schneller Code wird von verständlichen Aussagen getrennt und dann wird bewiesen, dass beides übereinstimmt.
Ein Prototyp der neuen Sprache liegt bisher nicht vor. Auch die genaue Syntax hat Buterin offengelassen. Es ist möglich, dass Entwickler sich auf einen gemeinsamen Standard einigen, vielleicht entstehen aber auch mehrere verschiedene Dialekte. Diese Entscheidung könnte bestimmen, wie schnell von KI geprüfter Code in produktive Systeme Einzug hält.
