Von 'Code Is Law' zu 'Spec Is Law': Wie formale Verifizierung die 3,4-Milliarden-Dollar-Exploit-Krise von DeFi beenden könnte

Ein einziger Rundungsfehler — ein Präzisionsverlust von weniger als einem Cent bei der Ganzzahldivision von Solidity — entzog Balancer auf neun Blockchains in weniger als 30 Minuten 128 Millionen US-Dollar. Die Pools waren jahrelang in Betrieb. Mehrere Audits hatten den Code überprüft. Niemand hat es bemerkt. Dies ist der Zustand der DeFi-Sicherheit im Jahr 2026: Milliarden von Dollar, die durch ein Paradigma geschützt werden, das nachweislich und wiederholt versagt hat.

Jetzt schlägt a16z crypto ein radikales Umdenken vor. In ihrem „Big Ideas“-Bericht für 2026 argumentiert die Risikokapitalgesellschaft, dass die Branche „Code Is Law“ — die grundlegende Überzeugung, dass bereitgestellter Smart-Contract-Code die ultimative Autorität ist — aufgeben und durch „Spec Is Law“ ersetzen muss, wobei mathematisch definierte Sicherheitseigenschaften zum durchsetzbaren Standard werden. Dieser Wandel könnte die Art und Weise, wie Protokolle erstellt, geprüft und verteidigt werden, grundlegend verändern.

Das 3,4-Milliarden-Dollar-Problem, das Audits nicht lösen können

Die Zahlen zeichnen ein vernichtendes Bild. Allein im Jahr 2025 verlor die Kryptowährungsbranche über 3,4 Milliarden US-Dollar durch Diebstahl, wobei die Kompromittierung von Bybit 1,5 Milliarden US-Dollar dieser Summe ausmachte. Fehler in Smart Contracts verursachten allein im ersten Halbjahr 2025 Schäden in Höhe von rund 263 Millionen US-Dollar. Insgesamt haben die größten DeFi-Exploits mehr als 10,77 Milliarden US-Dollar aus Protokollen extrahiert.

Das traditionelle Sicherheitsmodell — Code schreiben, Auditoren beauftragen, bereitstellen und hoffen — ist an seine Grenzen gestoßen. Selbst gut finanzierte Protokolle mit mehreren Audits von erstklassigen Firmen bleiben anfällig. Der Balancer-Exploit hat dies zweifelsfrei bewiesen: Eine Schwachstelle, die jahrelang offen dalag, von professionellen Sicherheitsüberprüfungen übersehen wurde und innerhalb von Minuten nach ihrer Entdeckung ausgenutzt wurde.

Beunruhigender ist die zunehmende Raffinesse der Angriffe. Flash-Loan-Exploits stiegen 2024 sprunghaft an und machten 83,3 % der relevanten Exploits aus. Die meisten großen Hacks im Jahr 2025 kombinierten zwei bis vier Schwachstellentypen gleichzeitig. Allein nordkoreanische Hacker stahlen im Jahr 2025 2,02 Milliarden US-Dollar, was einer Steigerung von 51 % gegenüber dem Vorjahr entspricht. Die Angreifer werden schneller intelligenter als die Verteidiger.

Anatomie eines 128-Millionen-Dollar-Rundungsfehlers

Der Balancer-Exploit verdient eine genaue Untersuchung, da er perfekt veranschaulicht, warum „Code Is Law“ scheitert. Am 3. November 2025 nutzte ein Angreifer eine mathematische Schwachstelle in der Art und Weise aus, wie die ComposableStablePools von Balancer Swaps mit geringem Wert handhaben.

Folgendes ist passiert: Wenn Token-Guthaben in einen bestimmten Bereich (8–9 Wei) gedrückt werden, verursacht die Ganzzahldivision von Solidity erhebliche Präzisionsverluste. Die Funktion _upscaleArray rundet beim Skalieren ab, was dazu führt, dass die Invariante des Pools — die mathematische Konstante, die faire Wechselkurse regeln sollte — unterschätzt wird. Dies drückt künstlich die Preise für BPT (Balancer Pool Token).

Der Angreifer instrumentalisierte dies durch die Ausführung einer dreistufigen Swap-Sequenz innerhalb einer einzigen batchSwap-Transaktion mit über 65 Operationen:

1. Preisunterdrückung: Tausch großer Mengen an BPT gegen zugrunde liegende Token, wodurch das Guthaben eines Tokens in den kritischen Schwellenwert von 8–9 Wei gedrückt wird, in dem Rundungsfehler maximiert werden.
2. Günstiger Erwerb: Minting oder Kauf von BPT zum künstlich unterdrückten Preis.
3. Vollständige Einlösung: Sofortige Einlösung von BPT gegen zugrunde liegende Vermögenswerte zum vollen Wert.

Der gesamte Angriff wurde innerhalb des Konstruktors eines bereitgestellten Smart Contracts ausgeführt — eine einzige Transaktion, die 128,64 Millionen US-Dollar über Ethereum, Base, Arbitrum, Avalanche, Optimism, Gnosis, Polygon, Berachain und Sonic hinweg abzog. Durch die schnelle Reaktion der Community konnten etwa 19 Millionen US-Dollar zurückgewonnen werden, aber der überwiegende Teil ging verloren.

Die entscheidende Lektion: Dies war keine exotische Schwachstelle. Es war eine Verletzung einer mathematischen Invariante — die Art von Fehler, die eine formale Spezifikation per Definition abgefangen hätte.

Was „Spec Is Law“ tatsächlich bedeutet

Der Vorschlag von a16z arbeitet auf zwei Ebenen: statisch (vor der Bereitstellung) und dynamisch (nach der Bereitstellung).

Auf der statischen Seite muss sich die DeFi-Sicherheit von der Überprüfung handverlesener lokaler Eigenschaften hin zum systematischen Nachweis globaler Invarianten bewegen. Anstatt zu fragen: „Behandelt diese Funktion Sonderfälle korrekt?“, lautet die Frage nun: „Behält dieses gesamte System seine mathematischen Kerneigenschaften unter allen möglichen Eingaben und Zuständen bei?“

Hier kommen formale Verifizierungstools wie Certora Prover und das K-Framework von Runtime Verification ins Spiel. Diese Tools vergleichen den Bytecode von Smart Contracts mit mathematischen Regeln, die das erwartete Verhalten definieren, und prüfen jeden möglichen Vertragszustand und Ausführungspfad. Certora Prover verwendet beispielsweise Spezifikationen, die in CVL (Certora Verification Language) geschrieben sind, um Eigenschaftsverletzungen durch statische Analyse und Constraint-Solving zu erkennen.

Auf der dynamischen Seite werden dieselben Invarianten zu aktiven Schutzplanken — Laufzeit-Assertionen, die jede Transaktion erfüllen muss. Wenn eine Transaktion eine grundlegende Sicherheitseigenschaft verletzen würde, wird sie automatisch rückgängig gemacht. Dies ist das Konzept der „letzten Verteidigungslinie“: Selbst ein neuartiger, bisher unbekannter Angriff muss dennoch die grundlegenden Sicherheitseigenschaften des Systems erfüllen.

Die Eleganz dieses Ansatzes liegt in seiner Asymmetrie. Angreifer müssen Verletzungen finden; Verteidiger müssen nur definieren, wie „korrekt“ aussieht. Wie a16z es ausdrückt: „Selbst ein neuartiger Angriff muss dieselben Sicherheitseigenschaften erfüllen, die das System intakt halten, sodass nur noch Angriffe übrig bleiben, die winzig oder extrem schwer auszuführen sind.“

Wer dies bereits so umsetzt

Die Vision „Spec is Law“ ist nicht rein theoretisch. Mehrere bedeutende Protokolle haben damit begonnen, die formale Verifizierung (Formal Verification) als Kernbestandteil ihres Entwicklungsprozesses zu übernehmen.

Aave, das nach TVL größte Lending-Protokoll, hat den Certora Prover direkt in seine Continuous Integration Pipeline integriert. Jede Codeänderung wird automatisch gegen formale Spezifikationen verifiziert, bevor sie gemergt werden kann. Dies ist kein gelegentliches Audit — es ist ein mathematischer Beweis, der bei jedem Commit ausgeführt wird.

Uniswap V2 wurde einer formalen Verifizierung seines zentralen „x * y = k“ Market-Maker-Modells unterzogen, wobei das K-Framework von Runtime Verification zum Einsatz kam. Die Verifizierung umfasste die Formalisierung des mathematischen Modells, die Smart-Contract-Implementierung und die symbolische Ausführung des kompilierten Bytecodes für vier kritische Funktionen.

Kamino, ein Solana-basiertes Lending-Protokoll, begann Anfang 2025 mit der Überprüfung kritischer Invarianten mittels Certora Prover. Das XRP Ledger hat ebenfalls Invarianten-Prüfungen auf Protokollebene implementiert. Dies sind keine exklusiven Entwicklungen für Ethereum — der „Spec is Law“ -Ansatz breitet sich über verschiedene Blockchain-Ökosysteme aus.

KI trifft auf formale Verifizierung: Certoras Composer

Eine der größten Barrieren für die formale Verifizierung war bisher ihre Komplexität. Das Schreiben formaler Spezifikationen erfordert spezialisiertes Fachwissen, das den meisten Entwicklungsteams fehlt. Das ändert sich gerade.

Im Dezember 2025 brachte Certora den AI Composer auf den Markt — eine Open-Source-KI-Coding-Plattform, die formale Verifizierung direkt in den Prozess der Code-Generierung einbettet. Im Gegensatz zu generischen KI-Coding-Tools, die Geschwindigkeit priorisieren, stellt der AI Composer sicher, dass jeder KI-generierte Codeschnipsel vor der Ausführung mathematischen Sicherheitsregeln entspricht.

Die Plattform stellt eine potenzielle Demokratisierung der formalen Verifizierung dar. Wenn KI beim Schreiben von Spezifikationen helfen, Invarianten vorschlagen und die Kosten für das manuelle Proof-Engineering senken kann, wird „Spec is Law“ über die Handvoll Teams hinaus zugänglich, die sich derzeit spezialisierte Ingenieure für formale Verifizierung leisten können.

Diese Fusion aus KI und Verifizierung adressiert auch die Beobachtung von a16z, dass die aktuelle DeFi-Sicherheit „systematisch globale Invarianten beweisen sollte, anstatt nur handverlesene lokale zu verifizieren“. KI kann den Spezifikationsraum umfassender untersuchen als menschliche Ingenieure und potenziell jene subtilen mathematischen Verletzungen aufdecken — wie den Rundungsfehler bei Balancer —, die einer manuellen Überprüfung entgehen.

Die rechtlichen und Governance-Implikationen

„Spec is Law“ hat Auswirkungen, die über den Code hinausgehen. Wenn ein Protokoll formale Spezifikationen veröffentlicht, die sein beabsichtigtes Verhalten definieren, könnten diese Spezifikationen zum rechtlichen Standard werden, an dem das Protokoll gemessen wird.

Unter einem „Code is Law“ -Regime gilt jeder Exploit von bereitgestelltem Code technisch gesehen als „wie vorgesehen“ — der Code tat genau das, wofür er programmiert wurde, selbst wenn dies nicht die Absicht der Entwickler war. Unter „Spec is Law“ definiert eine formale Spezifikation die Absicht. Protokollentwickler wären für Abweichungen von veröffentlichten Spezifikationen haftbar, jedoch nicht für jeden möglichen Exploit-Vektor, der außerhalb dieser Spezifikationen liegt.

Dies schafft einen klareren Verantwortungsrahmen. Hätte Balancer eine formale Spezifikation veröffentlicht, die besagt, dass Pool-Invarianten unabhängig von der Transaktionssequenzierung innerhalb definierter Grenzen bleiben müssen, wäre der Rundungsfehler-Exploit eine klare Verletzung der Spezifikation gewesen — und potenziell eine Grundlage für rechtliche Schritte oder Versicherungsansprüche.

Herausforderungen und Einschränkungen

Die „Spec is Law“ -These ist überzeugend, steht jedoch vor realen Hindernissen.

Vollständigkeit der Spezifikation ist die grundlegende Herausforderung. Wie spezifiziert man jede Eigenschaft, die von Bedeutung ist, formal? Spezifikationen werden von Menschen geschrieben, und Menschen können kritische Eigenschaften übersehen — genau wie Auditoren kritische Bugs übersehen. Eine Spezifikation, die nicht die richtigen Invarianten erfasst, vermittelt falsche Sicherheit.

Komposierbarkeitsrisiken fügen eine weitere Ebene hinzu. Der Wert von DeFi ergibt sich daraus, dass Protokolle miteinander interagieren. Die formale Verifizierung der Invarianten eines einzelnen Protokolls garantiert keine Sicherheit, wenn dieses Protokoll auf unerwartete Weise mit anderen kombiniert wird. Die Interaktionsoberfläche zwischen Protokollen bleibt ein weitgehend unspezifiziertes Neuland.

Performance und Kosten sind praktische Bedenken. Formale Verifizierung ist rechenintensiv. Die Überprüfung von Invarianten zur Laufzeit erhöht die Gaskosten bei jeder Transaktion. Für Hochfrequenz-Protokolle, die Tausende von Transaktionen pro Sekunde verarbeiten, fallen diese Kosten ins Gewicht.

Trägheit bei der Einführung könnte das größte Hindernis sein. Die meisten DeFi-Teams veröffentlichen Code unter intensivem Wettbewerbsdruck. Die Integration formaler Verifizierung in die Entwicklungspipeline verlangsamt die Bereitstellung. Bis der Markt verifizierte Protokolle mit höherem TVL oder niedrigeren Versicherungsprämien belohnt, bleibt der Anreiz zur Einführung schwach.

Der Weg nach vorne

Trotz dieser Herausforderungen ist die Richtung klar. Die Kosten von Exploits — 3,4 Milliarden US-Dollar im Jahr 2025, 10,77 Milliarden US-Dollar kumuliert — machen den Status quo unhaltbar. Versicherungsmärkte, institutionelles Kapital und regulatorische Rahmenbedingungen werden zunehmend nachweisbare Sicherheitsgarantien fordern.

Die Konvergenz von KI-gestützter Erstellung von Spezifikationen, ausgereiften Werkzeugen für die formale Verifizierung und Infrastruktur für die Durchsetzung zur Laufzeit senkt die Hürden für die Einführung. Wenn Aave den Certora Prover bei jedem Commit ausführen kann und Kamino Invarianten auf Solana prüft, haben die Werkzeuge den Sprung von der akademischen Forschung zur Produktionsinfrastruktur geschafft.

Die Entwicklung der Branche von „Code is Law“ zu „Spec is Law“ spiegelt ein Muster wider, das in jeder reifenden Ingenieursdisziplin zu beobachten ist: von „wir haben es gebaut und es scheint zu funktionieren“ hin zu „wir können mathematisch beweisen, dass es seine Spezifikation erfüllt“. Die Luftfahrt, die Kerntechnik und das Halbleiterdesign haben diesen Übergang alle durchlaufen. DeFi, wo über 100 Milliarden US-Dollar an TVL von mathematischer Korrektheit abhängen, ist überfällig.

Die Frage ist nicht, ob „Spec is Law“ zum Standard wird. Die Frage ist, wie viele Milliarden noch verloren gehen, bis es soweit ist.

BlockEden.xyz bietet Blockchain-API-Infrastruktur auf Unternehmensniveau, die DeFi-Anwendungen über mehrere Chains hinweg antreibt. Da die formale Verifizierung zum Branchenstandard wird, bildet eine zuverlässige Node-Infrastruktur das Fundament für verifizierte Protokollinteraktionen. Erkunden Sie unseren API-Marktplatz, um auf einer Infrastruktur aufzubauen, die für die Security-First-Ära entwickelt wurde.