Formale Verifikation fristete den größten Teil der Softwaregeschichte in einer kleinen, spezialisierten Nische: Flugsteuerungen, Herzschrittmacher-Firmware, Dinge, bei denen ein Fehler jemanden umbringt und es kein Patch am nächsten Dienstag gibt.

Alles andere lief auf Tests, Code-Reviews und dem angesammelten Vertrauen des Produktivbetriebs. Dieser Kompromiss war rational. Ein Programm zu beweisen ist langsam und teuer, und bei den meisten Software-Produkten kostet ein Fehler einen Rollback und einen Vorfallsbericht, keine Katastrophe. Tests fangen die Fehler ab, die wichtig genug sind, um abgefangen zu werden, und die Branche hat sich vierzig Jahre lang um genau diese Tatsache herum optimiert.

Finanzcode bricht diesen Kompromiss auf. Ein Abwicklungsvertrag bekommt kein Patch am Dienstag. Sobald er live ist und Werte hält, sind alle Pfade durch ihn aktiv, einschließlich der Pfade, die niemand getestet hat, und ein Angreifer braucht nur einen davon zu finden. Die Kosten eines unbewiesenen Fehlers sind kein Vorfallsbericht mehr, sondern der volle gefährdete Wert, entnommen auf einen Schlag, unumkehrbar, von wem auch immer den Code genauer gelesen hat als das Team, das ihn ausgeliefert hat.

Tests sagen, dass die Pfade funktionieren, an die man gedacht hat. Verifikation sagt, dass kein Pfad übrig ist, der es nicht tut.

Was sich praktisch geändert hat, ist die Zugänglichkeit. SMT-Solver, für die früher eine Promotion nötig war, laufen heute als Linter mit. Property-based-Testing-Frameworks erzeugen die feindseligen Eingaben, an die eine menschliche Prüferin nicht gedacht hätte. Leichtgewichtige Spezifikationssprachen erlauben es einem Team, eine Invariante zu formulieren, etwa "die Gesamtmenge ändert sich bei keiner Übertragung", und dafür einen maschinell geprüften Beweis zu bekommen, der für jede mögliche Eingabe gilt, nicht nur für die in der Testsuite. Das ist keine vollständige Programmverifikation im klassischen Sinn, und das muss es auch nicht sein. Es muss nur die Handvoll Eigenschaften abdecken, bei denen ein Irrtum nicht mehr rückgängig zu machen ist.

Die ehrliche Version dieser Geschichte lautet nicht, dass formale Methoden plötzlich einfach geworden sind. Sie lautet, dass die Kostenasymmetrie den Aufwand endlich rechtfertigt. Ein Team, das einen Checkout-Prozess ausliefert, greift weiterhin zuerst zu Tests, und das zu Recht. Ein Team, das Code ausliefert, der Werte in dem Moment abwickelt, in dem er läuft, kann sich Beweis nicht mehr als optional leisten, denn die Alternative ist, von der Angreiferin zu erfahren, welche Invariante falsch war, nicht vom Audit, das dafür eigentlich zuständig gewesen wäre.