Ethereum-Mitgründer Vitalik Buterin sieht eine bemerkenswerte Zukunft für die Softwareentwicklung. Seiner Ansicht nach könnte die Kombination aus künstlicher Intelligenz und formaler Verifikation letztlich zu Software führen, die sowohl extrem effizient als auch mathematisch überprüft sicher ist.
In einem neuen Blogbeitrag beschreibt Buterin, wie KI Programmierer sowohl beim Schreiben als auch beim Überprüfen komplexen Codes unterstützen kann. Besonders im Bereich Kryptografie, Ethereum-Infrastruktur, Konsensmechanismen und Zero-Knowledge-Systeme sieht er enormes Potenzial.
Gleichzeitig warnt Buterin davor, formale Verifikation als magische Lösung zu betrachten. Selbst mathematisch geprüfte Software kann Fehler enthalten, wenn die zugrunde liegenden Annahmen oder Spezifikationen falsch definiert wurden. Seine vollständige Analyse steht auf vitalik.eth.limo.
Ethereum ist erhältlich bei Bitvavo und Bybit.
KI soll Software sicherer machen
Laut Buterin wächst die Sorge, dass leistungsstarke KI-Modelle das Auffinden von Schwachstellen in Software immer einfacher machen. Einige Entwickler befürchten deshalb, dass vollständig sicherer Code letztlich unmöglich wird.
Buterin glaubt hingegen an das Gegenteil. Er erwartet, dass KI-Systeme Programmierern künftig dabei helfen werden, Code automatisch mithilfe mathematischer Beweise zu überprüfen. Dadurch könnten Fehler deutlich schneller entdeckt werden als mit traditionellen Softwaretests.
Der Ethereum-Mitgründer bezeichnet dies möglicherweise sogar als die „finale Form“ der Softwareentwicklung. Dabei schreibt die KI nicht nur den Code, sondern generiert gleichzeitig auch formale Nachweise dafür, dass die Software korrekt funktioniert.
Ethereum- und ZK-Systeme profitieren
Laut Buterin eignen sich insbesondere Blockchain-Systeme ideal für formale Verifikation. Dazu zählen Ethereum-Clients, Zero-Knowledge-Proofs, Smart Contracts und kryptografische Protokolle.
Er nennt unter anderem Projekte, die an vollständig verifizierten Implementierungen von ZK-Systemen und sogar kompletten Ethereum Virtual Machine-Umgebungen arbeiten. Dadurch können Entwickler mathematisch nachweisen, dass sich bestimmte Software exakt wie vorgesehen verhält.
Laut Buterin wird dies besonders wichtig, da KI immer leistungsfähiger darin wird, Bugs und Schwachstellen automatisch zu finden – insbesondere jetzt, da die Branche häufiger mit groß angelegten Hacks innerhalb des Ethereum-Ökosystems konfrontiert ist.
Auch Sicherheitsunternehmen und Browserentwickler würden seiner Ansicht nach zunehmend auf solche Techniken setzen, um Cyberangriffe zu verhindern.
Keine perfekte Lösung für Bugs
Dennoch sieht Buterin auch klare Grenzen. Formale Verifikation überprüft nämlich nur, ob Software den zuvor festgelegten Regeln und Spezifikationen entspricht. Wenn diese Regeln falsch definiert sind, können dennoch gefährliche Fehler entstehen.
Darüber hinaus bleiben Hardwareprobleme, Side-Channel-Angriffe und menschliche Fehler seiner Ansicht nach große Risiken innerhalb der Cybersicherheit.
Buterin erwartet deshalb, dass zukünftige Software zunehmend in einen kleinen, extrem sicheren Kern und eine größere Ebene mit weniger kritischen Anwendungen aufgeteilt wird. Besonders dieser sichere Kern könnte letztlich vollständig mithilfe von KI und formaler Verifikation überprüft werden.