a16z's „Rules as Law“-Vision: Wie KI-gestützte formale Verifizierung und Laufzeit-Guardrails die DeFi-Sicherheit neu gestalten
Im Dezember 2025 richteten Forscher von Anthropic einen KI-Agenten auf 405 real existierende, ausgenutzte Smart Contracts. Der Agent erstellte funktionierende Exploits für 207 davon – 51 % – und entzog dabei 550 Millionen .
Dieser einzelne Datenpunkt verdeutlicht die existenzielle Krise, vor der das dezentrale Finanzwesen (DeFi) im Jahr 2026 steht. Die 3,4 Milliarden $, die 2025 durch Krypto-Hacks verloren gingen, waren kein Mangel an Bemühungen – die meisten angegriffenen Protokolle waren auditiert worden, einige sogar mehrfach. Es war ein Versagen des Paradigmas. Und nun schlägt a16z Crypto einen radikalen Ersatz vor: Verabschieden Sie sich von „Code ist Gesetz“ (Code is Law) und begrüßen Sie „Spezifikation ist Gesetz“ (Spec is Law), wobei mathematisch bewiesene Sicherheitseigenschaften und Echtzeit-Laufzeit-Schutzmechanismen (Runtime Guardrails) die meisten Exploits strukturell unmöglich machen.
Der 3,4-Milliarden-Dollar-Weckruf
Die Zahlen aus dem Jahr 2025 sind erschütternd. Der Krypto-Diebstahl erreichte 3,4 Milliarden verantwortlich war – ein Rekord. Der Hack der Bybit-Börse in Höhe von 1,5 Milliarden $ machte 44 % der jährlichen Verluste aus. Nur drei Vorfälle machten 69 % des gesamten Diebstahls aus.
Doch vielleicht noch beunruhigender als die Schlagzeilen ist das, was auf der DeFi-Seite geschah. Im März 2025 entzog eine Reentrancy-Schwachstelle in einem großen DeFi-Protokoll 47 Millionen $ in weniger als 90 Sekunden. Der Vertrag war von drei verschiedenen Firmen geprüft worden. Alle drei hatten es übersehen.
Dieses Muster – auditiert, ausgenutzt, wiederholt – hat sich dutzende Male abgespielt. Traditionelle Audits sind Momentaufnahmen, die von menschlichen Prüfern durchgeführt werden, die, egal wie qualifiziert sie sind, nicht jede mögliche Zustandsänderung in einem komplexen Smart Contract erschöpfend verifizieren können. Sie finden gängige Muster. Sie übersehen neuartige Kombinationen. Und da KI die Entdeckung von Exploits exponentiell billiger macht, schrumpft der Fehlerspielraum für Verteidiger gegen null.
Von „Code ist Gesetz“ zu „Spezifikation ist Gesetz“
Der Satz „Code ist Gesetz“ ist seit der Gründung von Ethereum das philosophische Fundament von Krypto. Was auch immer der Smart Contract tut, ist per Definition korrekt. Der DAO-Hack von 2016 hat dieses Prinzip auf die Probe gestellt. Ein Jahrzehnt später argumentiert a16z Crypto, dass es an der Zeit ist, es vollständig in den Ruhestand zu schicken.
In ihrem Prognosebericht für 2026 schlagen die Forscher von a16z das vor, was sie „Spezifikation ist Gesetz“ nennen – ein Framework, in dem Protokolle Sicherheitseigenschaften (Spezifikationen) formal definieren und sie auf jeder Ebene durchsetzen, von der Verifizierung vor dem Deployment bis zur Ausführung zur Laufzeit. Die zentrale Erkenntnis: Selbst ein neuartiger, nie zuvor gesehener Angriff muss dieselben Sicherheitseigenschaften erfüllen, die das System intakt halten. Wenn diese Eigenschaften streng definiert und erzwungen werden, sind die einzigen Exploits, die überleben, „winzig oder extrem schwer auszuführen“.
Dies ist keine theoretische Übung. Es ist eine konkrete technische Vorschrift mit zwei komplementären Ebenen.
Ebene 1: Statische formale Verifizierung (Vor dem Deployment)
Die formale Verifizierung nutzt mathematische Beweise, um zu zeigen, dass ein Smart Contract bestimmte Eigenschaften unter allen möglichen Eingaben und Zustandsübergängen erfüllt – nicht nur unter denen, an die ein menschlicher Tester gedacht hat. Im Gegensatz zu Fuzzing oder Unit-Tests, die eine Teilmenge von Szenarien untersuchen, ist die formale Verifizierung erschöpfend.
Der Ansatz erfordert, dass Protokolle globale Invarianten definieren: Eigenschaften, die immer wahr sein müssen. Für ein Lending-Protokoll könnte eine Invariante lauten: „Der Gesamtwert der Sicherheiten muss immer den Gesamtwert der ausstehenden Kredite übersteigen.“ Für eine DEX: „Kein einzelner Swap darf mehr Wert extrahieren, als der Pool enthält.“
Certora, das führende Unternehmen für formale Verifizierung im Krypto-Bereich, demonstrierte 2025 die Leistungsfähigkeit dieses Ansatzes. In Zusammenarbeit mit Kamino Finance auf Solana evaluierte der Prover von Certora systematisch zwei Solvenz-Invarianten und deckte eine Präzisionsverlust-Schwachstelle auf – einen subtilen Rundungsfehler, der es Benutzern ermöglichte, mehr Sicherheiten einzulösen, als sie hinterlegt hatten. Kein menschlicher Auditor hatte dies bemerkt.
Branchenweit sicherte Certora im Jahr 2025 einen Gesamtwert von 196,5 Milliarden $ (Total Value Locked) ab und verhinderte, dass mehr als 720 Schwachstellen in die Produktion gelangten. Vierzehn der Top 20 DeFi-Protokolle nach TVL – etwa 70 % der Kategorie – arbeiten nun mit Certora zusammen. Der Certora Prover ist mittlerweile Open Source, und sein neues AI Composer-Tool nutzt maschinelles Lernen, um beim Schreiben von Spezifikationen und beim Vorschlagen von Invarianten zu helfen, wodurch der manuelle Aufwand, der die formale Verifizierung in der Vergangenheit unerschwinglich teuer machte, drastisch reduziert wird.
Ebene 2: Laufzeit-Schutzmechanismen (Nach dem Deployment)
Die statische Verifizierung findet Fehler vor dem Deployment. Aber was ist mit upgradefähigen Verträgen, Governance-Änderungen, Orakel-Ausfällen oder neuartigen Angriffsvektoren, die erst nach dem Start auftreten? Hier wird die Vision von a16z radikal.
Der Vorschlag: Kodieren Sie Sicherheitseigenschaften als Laufzeit-Assertionen (Runtime Assertions), die jede Transaktion erfüllen muss. Wenn eine Transaktion eine Invariante verletzen würde – zum Beispiel durch das Entziehen von mehr als einem protokollseitig definierten Prozentsatz eines Pools in einem einzigen Block –, wird die Transaktion automatisch rückgängig gemacht, bevor Zustandsänderungen festgeschrieben werden.
Betrachten Sie es als einen Schutzschalter für Smart Contracts. Eine traditionelle Finanzbörse stoppt den Handel, wenn die Volatilität Schwellenwerte überschreitet. Laufzeit-Schutzmechanismen tun dasselbe, jedoch durch Code erzwungen, in der Geschwindigkeit der Blockproduktion und ohne menschliches Eingreifen.
Guardrail, ein Startup, das genau diese Infrastruktur aufbaut, setzt über 295 anpassbare „Guards“ ein, die Anomalien erkennen, riskante Transaktionen simulieren und Laufzeitprüfungen erzwingen. Die Plattform schützt über 1,3 Milliarden $ an Vermögenswerten und kann automatisch anfällige Funktionen pausieren oder bösartige Wallets in Echtzeit markieren.
Die Forscher von a16z stellen fest, dass „in der Praxis fast jeder bisherige Exploit eine dieser Prüfungen während der Ausführung ausgelöst hätte, was den Hack potenziell gestoppt hätte“. Der 47-Millionen-Dollar-Reentrancy-Angriff? Eine einfache Invariantenprüfung des Pool-Guthabens vor und nach jeder Transaktion hätte ihn gestoppt. Der 1,5-Milliarden-Dollar-Bybit-Hack? Eine Laufzeitüberwachung der Abhebungsgeschwindigkeit und der Zieladressen hätte eine automatische Pause auslösen können.
Das KI-Wettrüsten: Offensive trifft auf Defensive
Die Dringlichkeit hinter diesem Paradigmenwechsel wird durch eine neue Realität vorangetrieben: KI macht Angriffe schneller billiger, als sie Verteidigungsmaßnahmen stärkt.
Die SCONE-bench-Forschung von Anthropic zeichnet ein ernüchterndes Bild. Ihre KI-Agenten, die gegen 405 reale, zwischen 2020 und 2025 exploitierte Contracts vorgingen, erreichten eine Erfolgsquote von 51 %. Bei Contracts, die nach Juni 2025 exploitiert wurden — was bedeutet, dass die KI keine Trainingsdaten zu diesen spezifischen Schwachstellen hatte —, erzeugten Claude Opus 4.5, Claude Sonnet 4.5 und GPT-5 dennoch Exploits im Gesamtwert von $ 4,6 Millionen.
Besonders auffällig: Als diese Agenten auf 2.849 kürzlich bereitgestellte Contracts ohne bekannte Schwachstellen angesetzt wurden, entdeckten sie zwei echte Zero-Day-Exploits. Die Exploit-Einnahmen aus gestohlenen simulierten Geldern haben sich etwa alle 1,3 Monate verdoppelt, während die Rechenkosten pro erfolgreichem Exploit in sechs Monaten um mehr als 70 % gesunken sind.
Diese exponentielle Verbesserung der offensiven KI-Fähigkeiten bedeutet, dass das alte Sicherheitsmodell — Auditoren einstellen, einen Bericht erhalten, bereitstellen, beten — strukturell unzureichend ist. Das a16z-Framework adressiert dies, indem es eine Verteidigung schafft, die sich mit der Geschwindigkeit der Spezifikation verbessert, nicht mit der Geschwindigkeit menschlicher Code-Reviews.
KI treibt auch die defensive Seite voran. Der AI Composer von Certora, der im Dezember 2025 in der Alpha-Version veröffentlicht wurde, ist die erste KI-Coding-Plattform, die formale Verifizierung direkt in den Code-Generierungsprozess integriert. Speziell entwickelte KI-Sicherheitsagenten haben in kontrollierten Studien Erkennungsraten von 92 % für Schwachstellen gezeigt. Das Audit von 2026 ist nicht vollautomatisiert — es ist ein menschlicher Experte, der von einer KI-Analyse geleitet wird, die in der halben Zeit das Zehnfache an Umfang abdeckt.
Reale Akzeptanz: Wer baut auf diese Weise?
Der Übergang von der Theorie zur Praxis ist bereits in vollem Gange.
Aave V4 stellt die umfassendste Implementierung von mehrschichtiger Sicherheit in der Geschichte von DeFi dar. Die Sicherheitsüberprüfung des Protokolls erstreckte sich über etwa ein Jahr, von Anfang 2025 bis Februar 2026, mit einem vom DAO genehmigten Budget von $ 1,5 Millionen. Certora arbeitete von den frühesten Designphasen an mit den Entwicklern zusammen und führte formale Verifizierungen sowie Invarianten-Tests durch, während ChainSecurity, Trail of Bits und Blackthorn mehrere Runden manueller Audits durchführten. Das Ergebnis: ein Protokoll, bei dem Sicherheitseigenschaften vor dem Deployment mathematisch verifiziert und danach kontinuierlich überwacht werden.
Kamino Finance auf Solana begann mit der Überprüfung kritischer Invarianten unter Verwendung des Certora Provers und fing so die Sicherheitslücke durch Präzisionsverlust ab, die eine Über-Rückzahlung von Sicherheiten ermöglicht hätte — genau die Art von Grenzfall, den menschliche Auditoren historisch übersehen.
Das Sui-Ökosystem setzt auf formale Verifizierung auf Sprachebene, wobei der Sui Prover Open Source wurde, um mathematische Verifizierung — dieselbe Technik, die in Flugsteuerungssystemen und Prozessordesigns verwendet wird — in die tägliche Smart-Contract-Entwicklung auf der Move VM zu bringen.
Guardrail operationalisiert die Durchsetzung zur Laufzeit (Runtime Enforcement) für Produktionsprotokolle und verwandelt das theoretische „Circuit Breaker“-Konzept in eine implementierte Infrastruktur, die reale Vermögenswerte schützt.
Die verbleibende Lücke
Trotz dieser Fortschritte bleibt eine kritische Lücke bestehen. Es gibt keine globale Anforderung, dass Protokolle mit hohem TVL kontinuierliche Adversarial Testings, Runtime Enforcement oder Agenten-gestütztes Monitoring durchführen müssen. Ein Protokoll kann immer noch ohne Laufzeitüberwachung an den Start gehen, und Nutzer können weiterhin Milliarden basierend auf einem Audit-PDF und einem Badge einzahlen.
Der Versicherungsmarkt könnte die Änderung erzwingen, die durch freiwillige Übernahme bisher ausblieb. Da die KI-gestützte Exploit-Suche zugänglicher wird, beginnen Versicherungsprotokolle, KI-Monitoring als Voraussetzung für den Versicherungsschutz zu verlangen. Bug-Bounty-Plattformen integrieren KI-Agenten als Erstprüfer. Die ökonomische Logik ist simpel: Wenn KI Exploits für $ 1,22 finden kann, sind die Kosten dafür, keine defensive KI einzusetzen, astronomisch.
Die gedämpften Hack-Verluste von DeFi Ende 2025 — trotz steigendem TVL — deuten auf bedeutende Fortschritte hin. Chainalysis bezeichnete dies als eine „entscheidende Abweichung von früheren Zyklen, in denen steigendes TVL normalerweise mehr erfolgreiche Angriffe bedeutete“. Doch die Bedrohung entwickelt sich weiter. Die TraderTraitor-Gruppe aus Nordkorea hat sich von Protokoll-Exploits auf Angriffe auf Cloud-Infrastrukturen verlagert. Social Engineering übertrifft mittlerweile Smart-Contract-Exploits als primären Angriffsvektor im Kryptobereich. Der Sicherheitsperimeter erweitert sich, und die formale Verifizierung von Smart Contracts ist zwar notwendig, aber nicht ausreichend.
Was „Spec is Law“ für die Zukunft von DeFi bedeutet
Die Vision von a16z würde, wenn sie vollständig umgesetzt wird, grundlegend ändern, was es bedeutet, ein DeFi-Protokoll bereitzustellen. Vor dem Start würde jede kritische Sicherheitseigenschaft formal bewiesen — nicht nur getestet oder auditiert, sondern mathematisch nachgewiesen, dass sie unter allen möglichen Bedingungen Bestand hat. Nach dem Start würden Laufzeit-Leitplanken (Runtime Guardrails) diese Eigenschaften in Echtzeit erzwingen und jede Transaktion automatisch rückgängig machen, die die Integrität des Protokolls gefährdet.
Dies ist nicht „schnell handeln und Dinge kaputt machen“. Es ist das Gegenteil: präzise handeln und beweisen, dass nichts kaputt gehen kann. Der Ansatz spiegelt wider, wie die Luftfahrt- und Halbleiterindustrie mit Sicherheit umgehen — durch formale Methoden, die keinen Raum für „wir glauben, dass es funktioniert“ lassen.
Die DeFi-Sicherheitslandschaft von 2026 spaltet sich auf. Auf der einen Seite: Protokolle, die Sicherheit als bloßes Häkchen betrachten, sich auf punktuelle Audits verlassen und hoffen, dass KI-gestützte Angreifer nicht finden, was menschliche Auditoren übersehen haben. Auf der anderen Seite: Protokolle, die Sicherheit in ihre Architektur einbetten und formale Verifizierung sowie Runtime Enforcement nutzen, um ganze Klassen von Exploits strukturell unmöglich zu machen.
Die im Jahr 2025 verlorenen $ 3,4 Milliarden sind die Kosten des alten Ansatzes. Das „Spec is Law“-Framework ist die Wette von a16z, dass die Branche es besser machen kann — und muss.
Der Aufbau auf einer Blockchain-Infrastruktur erfordert Fundamente, denen Sie vertrauen können. BlockEden.xyz bietet RPC- und API-Dienste der Enterprise-Klasse für Ethereum, Sui, Aptos und über 20 weitere Chains — die Art von zuverlässiger Infrastruktur, die sicherheitsbewusste Entwickler benötigen. Erkunden Sie unseren API-Marktplatz, um auf Fundamenten aufzubauen, die für die Ewigkeit ausgelegt sind.