Waarom kan ik code wel toetsen aan een specificatie, maar de specificatie zelf niet?

Formele verificatie van slimme contracten toont aan dat de code voldoet aan een schriftelijke specificatie, maar kan niet vaststellen of die specificatie daadwerkelijk het beoogde gedrag van het contract weergeeft. Uit een MDPI-onderzoek uit 2025 naar de modernste geautomatiseerde audittools bleek dat deze slechts 8 tot 20 procent van de exploiteerbare bugs in de productieomgeving detecteren, terwijl ze een dekking van meer dan 90 procent rapporteren voor syntaxispatronen op laag niveau. De kloof zit in de specificatie: logische fouten, voorwaarden voor het vergrendelen van activa en aannames over orakels komen bijna nooit voor in specificaties, omdat ingenieurs niet weten hoe ze deze moeten opsommen voordat een exploit de noodzaak ervan aantoont. Het PropertyGPT-artikel van NDSS 2025 stelt rechtstreeks dat de gemeenschap nog steeds geen geautomatiseerde generatie van uitgebreide eigenschappen heeft voor effectieve formele verificatie. Elke audit die een contract goedkeurt op basis van een onvolledige specificatie, leidt tot een vals gevoel van zekerheid in plaats van tot veiligheid