Formal Verification

Formal verification behandelt das Verhalten eines Programms als mathematisches Objekt: Statt einen Smart Contract gegen eine Handvoll Testfälle laufen zu lassen, schreiben Engineers eine präzise Spezifikation jedes Zustands, den der Code erreichen darf, und nutzen anschließend Theorem Prover oder automatisierte Solver, um lückenlos zu zeigen, dass die kompilierte Logik diese Spezifikation niemals verletzen kann. Die Technik existiert seit Jahrzehnten vor Krypto, am bekanntesten durch den maschinell geprüften Beweis des seL4-Betriebssystem-Mikrokernels aus dem Jahr 2009, und wurde seither auf Solidity-, Vyper-, Rust- und Move-Contracts übertragen, etwa mit Tools wie dem Certora Prover, der KEVM-Semantik des K Framework und dem eingebauten SMTChecker von Solidity.

In der Praxis übersetzt ein Verification Engineer die beabsichtigten Regeln eines Protokolls, etwa "die total supply überschreitet nie den Cap" oder "Collateral kann nicht unter der Liquidationsschwelle abgehoben werden", in eine Spezifikationssprache. Ein automatisierter Solver durchsucht dann den gesamten Raum möglicher Eingaben und Zustände nach einem Gegenbeispiel. Existiert keines, gilt die Eigenschaft als bewiesen und nicht nur als in Stichprobentests beobachtet. Diese Erschöpfung ist der Grund, warum formal verification zunehmend für hochwertige DeFi-Kreditmärkte, Stablecoins und Cross-Chain-Bridges verlangt wird, bei denen ein übersehener Rechenfehler oder Reentrancy-Pfad in der Vergangenheit zu Exploits im Wert von zig Millionen Dollar geführt hat.

Der Kompromiss liegt bei Kosten und Umfang. Eine korrekte Spezifikation zu schreiben erfordert ebenso viel Fachwissen wie das Schreiben des Contracts selbst, Verifikationsläufe können Tage an Engineering-Zeit kosten, und ein Beweis garantiert nur die tatsächlich spezifizierten Eigenschaften. Deshalb ergänzt formal verification ein klassisches Security Audit und Fuzz Testing, statt sie zu ersetzen, und wird meist nur für die kleine Teilmenge an Code eingesetzt, bei der ein Exploit katastrophale Folgen hätte.