Buterin sagt, dass KI-gestützte formale Verifikation die Sicherheit von Krypto erhöht

Buterin veröffentlicht neuen Beitrag über KI und Codesicherheit

Der Ethereum-Mitbegründer Vitalik Buterin veröffentlichte am 18. Mai 2026 einen Blogbeitrag auf vitalik.eth.limo. Darin argumentiert er, dass KI-gestützte formale Verifikation eines der wichtigsten Werkzeuge der Cybersicherheit werden wird. Die formale Verifikation ist eine Methode, die mathematische Beweise verwendet, um zu bestätigen, dass Software genau wie beabsichtigt funktioniert. Buterin erklärt, dass die Kombination von KI mit formaler Verifikation Entwicklern helfen wird, Schwachstellen zu finden, bevor Angreifer dies tun.

Claude Mythos als Beispiel für die Macht der KI genannt

Buterin nennt Claude Mythos, ein KI-Modell, das von Anthropic entwickelt wurde, als Beispiel für zunehmend leistungsfähige KI-Systeme. Er argumentiert, dass solche Systeme die Entdeckung und Ausnutzung von Schwachstellen beschleunigen können. Claude Mythos ist ein echtes Modell. Anthropic bestätigte seine Existenz nach einem versehentlichen Datenleck im März 2026. Eine Vorschau des Modells wurde im April 2026 an ausgewählte Partner veröffentlicht.

Buterin listet die Grenzen der formalen Verifikation auf

Buterin betont, dass die formale Verifikation nicht alle Risiken beseitigt. Beweissysteme können kritische Annahmen übersehen oder es versäumen, Hardware-Schwachstellen und angrenzende Angriffsflächen abzudecken. Er warnt auch, dass KI die Hürde zur Erstellung großer Softwaremengen senkt. Dies erhöht das Risiko, dass unsichere oder schlecht verstandene Codes in Produktionssysteme gelangen. Trotz dieser Grenzen argumentiert Buterin, dass der Ansatz das katastrophale Risiko im Vergleich zur traditionellen Softwareentwicklung verringert.

Arklib-Projekt zielt auf verifizierte STARK-Implementierung ab

Buterin hebt Arklib als ein konkretes Beispiel für formale Methoden an Ethereum hervor. Arklib ist ein Open-Source-Projekt, das darauf abzielt, eine vollständig formal verifizierte Implementierung eines STARK-Beweissystems zu erstellen. Ein STARK ist eine Art kryptografischer Beweis, der in der Skalierungsinfrastruktur von Ethereum verwendet wird. Die Ethereum Foundation finanzierte Nethermind, um Arklib mit der Formalisierung des FRI-Protokolls im Lean-Beweisassistenten zu erweitern. Buterin verweist auch auf formal verifizierte Implementierungen der Ethereum Virtual Machine, die direkt in RISC-V-Assembly geschrieben sind.