Glossary
Formale Verifikation
Mathematisch beweisen — nicht nur testen —, dass ein Smart Contract eine präzise Spezifikation erfüllt, mit Werkzeugen wie Certora, K oder Beweis-Assistenten.
Formale Verifikation ersetzt Testen durch Beweis. Der Engineer schreibt eine Spezifikation („das Gesamtangebot entspricht der Summe der Salden", „kein Aufrufer kann mehr als seinen Saldo abziehen") und ein Verifikationswerkzeug beweist entweder, dass die Spezifikation für jeden möglichen Input gilt, oder produziert ein Gegenbeispiel.
Werkzeuge wie Certora Prover, Halmos, KEVM und dedizierte Beweis-Assistenten (Coq, Lean, Isabelle) werden für die sicherheitskritischsten Contracts eingesetzt: Maker, Aave, Compound, Lido. Die Kosten sind hoch — die Spezifikation korrekt zu schreiben ist ein eigenes Engineering-Vorhaben —, doch für Milliarden-Dollar-Contracts wird es zunehmend zum Standard.