Formele verificatie

Formele verificatie is het wiskundig bewijzen dat een programma of een stel regels klopt. Bij gewoon testen probeer je een aantal situaties uit en kijk je of het goed gaat. Situaties die je niet bedenkt, controleer je ook niet. Bij formele verificatie bewijs je dat iets voor alle mogelijke situaties werkt.

Het is te vergelijken met een bouwkundige die niet alleen een brug test met een paar auto's, maar met een berekening laat zien dat hij elk toegestaan gewicht aankan.

Hoe werkt het?

Eerst wordt precies opgeschreven wat er moet kloppen, bijvoorbeeld: dit programma loopt bij geen enkel bestand vast. Dan komt er een bewijs: een uitwerking, stap voor stap, waarom dat zo is. Zo'n bewijs kan enorm zijn, soms honderdduizenden regels. Een mens leest dat niet na. Daarom doet een klein controleprogramma dat. Het rekent elke stap na, en keurt het hele bewijs af zodra één stap niet klopt. Wie het resultaat wil vertrouwen, hoeft alleen dat controleprogramma te vertrouwen en de afspraak over wat bewezen moest worden.

Een bewijs geldt wel precies voor wat is afgesproken. Het zegt niet dat een programma overal foutloos is, alleen dat het binnen de afspraak blijft.

Waarom het ertoe doet

Naarmate AI meer software schrijft en nakijkt, wordt het lastiger om alles zelf na te lezen. Formele verificatie laat de AI zelf een bewijs meeleveren. Anthropic liet Claude bij 123 veelgebruikte softwarebouwstenen een wiskundig bewijs meeleveren dat een klein programma stap voor stap controleert, en daarbij kwamen honderden verborgen fouten naar boven (link).

Ook voor veiligheid is het nuttig. Nvidia laat AI-agents in een afgeschermde ruimte werken en controleert de regels vooraf met zo'n wiskundige methode, zodat die niet meer toestaan dan bedoeld (link).