Laut Vitalik Buterin könnte die KI-gestützte formale Verifizierung die „endgültige Form“ von Software sein und es Ethereum ermöglichen, hochoptimierten Code mit maschinell überprüften Korrektheitsnachweisen zu liefern.
Zusammenfassung
- Vitalik Buterin argumentierte, dass die KI-gestützte formale Verifizierung eine „endgültige Form“ der Softwareentwicklung darstellen könnte, bei der der Code sowohl hocheffizient als auch mathematisch verifiziert sei.
- Er hob Anwendungen in der Kern-Roadmap von Ethereum hervor, darunter ZK-EVMs, STARK-Beweise, Konsens und quantenresistente Kryptographie, und betonte gleichzeitig, dass die formale Verifizierung zwar wirkungsvoll, aber kein Allheilmittel sei.
- Die Kommentare bauen auf seinen früheren Forderungen auf, etwa die Hälfte der Produktivitätssteigerungen der KI in Tests und formale Verifizierung zu stecken, um nahezu fehlerfreien Kryptocode zu einer realistischen Erwartung zu machen.
Ethereum (ETH) Mitbegründer Vitalik Buterin hat gesagt, dass die Kombination künstlicher Intelligenz mit formaler Verifizierung die „endgültige Form“ der Softwareentwicklung werden könnte, die es Entwicklern ermöglicht, hochoptimierten Code zu liefern, der auch durch maschinenüberprüfbare Korrektheitsnachweise gestützt wird. In einem neuen Aufsatz auf seiner persönlichen Website schreibt er, dass die formale Verifizierung „besonders gut für Situationen geeignet ist, in denen das Ziel viel einfacher ist als die Implementierung“, und verweist auf quantenresistente Signaturen, STARKs, Konsensalgorithmen usw ZK-EVMs als Spitzenkandidaten.
Vitalik: AI+ erweist sich als neuer Entwicklungs-Stack
Buterins jüngste Kommentare spiegeln einen Beitrag vom Februar wider, in dem er vorschlug, dass KI „dazu beitragen könnte, dass nahezu fehlerfreier Kryptocode eine realistische Erwartung darstellt“, vorausgesetzt, das Ökosystem kanalisiert etwa die Hälfte der Geschwindigkeitsgewinne der KI in stärkere Tests und Verifizierungen. In diesem Artikel warnte er Entwickler davor, Magie von KI-generiertem Code zu erwarten, und sagte, sie sollten „nicht davon ausgehen, dass man in der Lage sein wird, eine einzige Eingabeaufforderung einzugeben und in absehbarer Zeit eine hochsichere Version herauszubringen; es WIRD eine Menge Probleme mit Fehlern und Inkonsistenzen zwischen Implementierungen geben.“
Parallel dazu hat er praktische Beweise dafür hervorgehoben, dass KI-gestützte formale Methoden bereits in freier Wildbahn funktionieren, und zitierte das Lean Ethereum-Projekt, bei dem „ein Mitarbeiter … es geschafft hat, einen maschinenüberprüfbaren Beweis für einen der komplexesten Theoreme, auf die sich STARKs aus Sicherheitsgründen verlassen, KI-kodiert.“ Dieses Experiment, so schlug er vor, deutet auf eine Zukunft hin, in der KI-Tools Entwicklern dabei helfen, gewünschte Eigenschaften in einer Beweissprache auszudrücken und dann automatisch nach Beweisen dafür zu suchen und diese zu prüfen, dass eine bestimmte Implementierung sie tatsächlich erfüllt.
Sicherheitsupgrade, keine Sicherheitsgarantie
Trotz seiner Begeisterung hat Buterin wiederholt darauf hingewiesen, dass selbst eine perfekte formale Verifizierung auf einer Ebene nicht garantieren kann, dass sich ein gesamtes System wie beabsichtigt verhält. In seinem neuen Beitrag stellt er fest, dass „formale Verifizierung kein Allheilmittel ist“, und fügt hinzu, dass Entwickler, um wirklich durchgängig zu sein, alles verifizieren müssten, von der High-Level-Spezifikation bis hin zur RISC-V-Implementierung oder Beweiserarithmetisierung, „aber keine Sorge – das gibt es auch.“
Anfang des Jahres formulierte er Kryptosicherheit als das Problem der „Minimierung der Kluft zwischen Benutzerabsicht und Systemverhalten“ und argumentierte in einem separaten Aufsatz, dass „perfekte Sicherheit“ unmöglich sei, weil die menschliche Absicht selbst chaotisch und schwer zu formalisieren sei. Aus diesem Grund plädiert er für Redundanz – Simulationen, Multisig, formale Verifizierung und mehrere Client-Implementierungen – statt nur für zusätzliche Reibungsverluste. Er sagt, dass bestimmte Sicherheitsansprüche in vielen Kontexten immer noch bewiesen werden können und „über 99 % der negativen Folgen von fehlerhaftem Code vermieden werden“.
Buterin vertritt den Standpunkt, dass KI sowohl zur Beschleunigung der Roadmap von Ethereum als auch zur gleichzeitigen Erhöhung der Sicherheitslatte eingesetzt werden sollte, anstatt Geschwindigkeit und Sicherheit als gegensätzliche Ziele zu betrachten. „Die Leute sollten der Möglichkeit (nicht der Gewissheit! Möglichkeit) gegenüber offen sein, dass die Ethereum-Roadmap viel schneller fertig wird, als die Leute erwarten, und das mit einem viel höheren Sicherheitsstandard, als die Leute erwarten“, schrieb er und warnte gleichzeitig, dass Entwickler auch in einem noch immer Fehler und Randfälle durcharbeiten müssen KI‑plus‑formelle‑Verifizierung der Zukunft.
