Formal Verification

Formal verification behandelt het gedrag van een programma als een wiskundig object: in plaats van een smart contract te draaien tegen een handvol testgevallen, schrijven engineers een precieze specificatie van elke toestand die de code mag bereiken, en gebruiken vervolgens theorem provers of geautomatiseerde solvers om uitputtend aan te tonen dat de gecompileerde logica die specificatie nooit kan schenden. De techniek bestaat al decennia voor crypto, met als bekendste voorbeeld het machinaal gecontroleerde bewijs uit 2009 van de seL4-operating-system-microkernel, en is sindsdien toegepast op Solidity-, Vyper-, Rust- en Move-contracten via tools zoals de Certora Prover, de KEVM-semantiek van het K Framework, en de ingebouwde SMTChecker van Solidity.

In de praktijk vertaalt een verificatie-engineer de beoogde regels van een protocol, zoals "de total supply overschrijdt nooit de cap" of "collateral kan niet worden opgenomen onder de liquidatiedrempel", naar een specificatietaal, waarna een geautomatiseerde solver de volledige ruimte van mogelijke inputs en toestanden doorzoekt naar een tegenvoorbeeld. Bestaat dat niet, dan is de eigenschap bewezen in plaats van alleen waargenomen in een steekproef van tests. Deze uitputtendheid is de reden dat formal verification steeds vaker verplicht wordt bij DeFi-leenmarkten, stablecoins en cross-chain bridges met hoge waarde, waar een over het hoofd geziene rekenkundige edge case of reentrancy-pad in het verleden tot exploits van tientallen miljoenen dollars heeft geleid.

De keerzijde is kosten en reikwijdte. Het schrijven van een correcte specificatie vereist evenveel domeinkennis als het schrijven van het contract zelf, verificatieruns kunnen dagen aan engineeringtijd kosten, en een bewijs garandeert alleen de eigenschappen die daadwerkelijk zijn gespecificeerd. Daarom vult formal verification een traditionele security audit en fuzz testing aan in plaats van deze te vervangen, en wordt het doorgaans gereserveerd voor de kleine subset code waar een exploit catastrofaal zou zijn.