Nu steeds meer software door AI wordt geschreven, groeit de vraag hoe je weet dat die code klopt. Een oud en berucht arbeidsintensief antwoord beleeft daardoor een comeback: formele verificatie. Daarbij leg je eerst precies vast wat een programma moet doen en bewijs je daarna wiskundig dat de code zich daaraan houdt. WIRED beschrijft hoe een groeiende groep start-ups, waaronder het nieuwe &Truth, dat proces met AI wil automatiseren.

Hoe het werkt

Het lastigste deel is de specificatie: de regels waaraan code moet voldoen. Een simpel voorbeeld uit het stuk: een tabel moet na het sorteren dezelfde items bevatten als ervoor, alleen in een andere volgorde. De start-ups willen AI vooral inzetten om zulke specificaties op te stellen. Andere software zet de code daarna om naar een vorm die bewijsprogramma's als Lean, Rocq en Isabelle kunnen controleren.

Wie er al mee werkt

  • Apple meldde eerder dit jaar dat formele verificatie fouten in zijn encryptiebibliotheek corecrypto vond die op geen andere manier boven water waren gekomen. Wel moet het bedrijf voorzichtig zijn met nieuwe code, omdat het controleren tijd kost.
  • De non-profit Beneficial AI Foundation gebruikte een subsidie van Anthropic om de veelgebruikte open-sourcebibliotheek curve25519-dalek te verifiëren.
  • Madan Musuvathi vertrok na ruim twintig jaar bij Microsoft Research om de start-up Truidic op te richten. Incidenten zoals de hack van Hugging Face door OpenAI-agents overtuigden hem dat het haast heeft.
  • Proofcraft, een van de weinige bedrijven die al langer verificatie verkoopt, krijgt naar eigen zeggen meer aanvragen dan de hele sector aankan.

Niet blind vertrouwen

Er zijn ook twijfels. Twee beveiligingsbestuurders van grote bedrijven zeggen tegen WIRED niet zeker te weten of automatisering verificatie de moeite waard maakt, al zouden ze wel willen betalen voor "geverifieerde" AI-code van grote AI-labs. Proofcraft-topvrouw June Andronick en hoofdwetenschapper Gerwin Klein waarschuwen dat specificaties die door AI zijn geschreven tot "onterecht vertrouwen" kunnen leiden. Als de regels zelf niet kloppen, bewijst het bewijs weinig.

Ook de financiering is een open vraag. Michael Rosenberg, beheerder van curve25519-dalek, hoopt op duurzame steun voor verificatie van open-sourcecode, maar zegt dat de sector niet moet leunen op de goodwill van AI-bedrijven.

Voor Europa is het onderwerp niet abstract. De Cyber Resilience Act verplicht makers van software met digitale onderdelen straks om beveiliging aantoonbaar op orde te hebben. Wie veel AI-code gebruikt, zoekt manieren om dat te onderbouwen, en verificatie is daar een van. Eerder schreven we al dat onderzoekers vinden dat AI-agents te weinig sporen nalaten voor toezicht.