Formele Verificatie & Bewijsautomatisering

Testen bemonstert gedrag; veiligheid vereist garanties over elke mogelijke input. Formele verificatie overbrugt die kloof met wiskundig bewijs in plaats van statistisch vertrouwen — en voor AI-systemen die op weg zijn naar gecertificeerde, veiligheidskritische implementaties, is bewijs steeds vaker het enige bewijsmateriaal dat standhoudt.

Waarom testen bugs vindt maar ze niet kan elimineren

Meer dan 60% van de eerste semiconductor-ontwerpen vereist een silicon respin ondanks maanden van op simulatie gebaseerde tests. Elke respin op 3nm kost $40M aan alleen al maskersets. Het kernprobleem is wiskundig: testen bemonstert gedrag, maar veiligheid vereist garanties over alle mogelijke inputs. Formele verificatie biedt die garanties via wiskundig bewijs, niet via statistisch vertrouwen.

Onze aanpak is het bouwen van verificatiepipelines — zoals onze werkende demo van AI-gestuurde semiconductorverificatie — ontworpen om te bewijzen dat eigenschappen van AI-systemen universeel gelden:

• Robuustheidscertificering voor neurale netwerken
• Model checking voor protocollen van agent-orkestratie
• Door stellingbewijzers ondersteunde veiligheidsargumenten voor DO-178C en ISO 26262 certificeringspakketten

De verificatietechniek wordt afgestemd op de eigenschap en het systeem: volledige verificateurs waar haalbaar, sounde incomplete methoden waar schaalvergroting dit vereist, en altijd een heldere verantwoording van wat bewezen is versus wat getest is.

Verificatie van neurale netwerken: wat echt werkt in 2026

Het vakgebied heeft een duidelijke leider. alpha-beta-CROWN heeft VNN-COMP (de Verified Neural Network Competition) gewonnen gedurende vijf opeenvolgende jaren, van 2021 tot en met 2025, waarbij het als eerste eindigde in elke beoordeelde benchmark. Het combineert GPU-versnelde lineaire bound propagation met branch-and-bound-zoekmethoden om eigenschappen zoals adversariële robuustheid, monotoniciteit en outputbereikgrenzen te verifiëren op convolutionele netwerken met miljoenen parameters. Voor de eigenschappen die van cruciaal belang zijn bij veiligheidskritische implementaties, is dit het startpunt op productieniveau:

• Bewijzen dat geen enkele perturbatie binnen een gedefinieerde epsilon-bal de classificatie verandert
• Bewijzen dat het verhogen van een feature de output alleen in de gespecificeerde richting kan bewegen
• Bewijzen dat outputs binnen fysiek zinvolle bereiken blijven

Marabou 2.0, de krachtigste CPU-gebaseerde verificateur, maakt gebruik van SMT-gebaseerd redeneren en genereert UNSAT-certificaten via het Farkas-lemma, wat archiveerbare bewijsartefacten oplevert voor certificeringsdossiers. Het levert 2x–10x snelheidsverbeteringen ten opzichte van zijn voorganger, waarbij het mediane piekgeheugen daalt van 604MB naar 59MB.

De eerlijke restrictie: de verificatie van neurale netwerken is NP-compleet. De keuze tussen volledige en sounde incomplete methoden is een fundamentele afweging tussen precisie en schaalbaarheid, die we per traject bepalen op basis van de netwerkarchitectuur, de te certificeren eigenschappen en hoe het bewijsmateriaal gebruikt zal worden.

Neural Abstract Interpretation (ICLR 2025) behaalt analyses onder 0,7 seconden op netwerken met een miljoen neuronen — maar de afweging tussen precisie en schaalbaarheid blijft fundamenteel.

Bewijsautomatisering doorbreekt de kostendrempel

De verificatie van de seL4-microkernel kostte circa 20 mensjaren : 9.000 regels C vereisten 200.000 regels bewijs, ongeveer 23 regels bewijs per regel implementatie. Die verhouding maakte formele verificatie economisch onhaalbaar voor de meeste software. De economische dynamiek veranderde in 2025–2026.

AI-ondersteunde stellingbewijzers genereren nu bewijzen tegen een fractie van de kosten:

• BFS-Prover-V2 behaalt 95.08% op de miniF2F-benchmark.
• Leanstral van Mistral (uitgebracht in March 2026) is de eerste open-source AI-agent voor Lean 4-verificatie, tegen 92x lagere kosten dan toonaangevende grensverleggende LLM's.
• Aristotle van Harmonic (waardering van $1,45 miljard) genereert en verifieert formeel Lean 4-bewijzen, waarmee het prestaties op gouden medaille-niveau levert op IMO-wiskundevraagstukken.

Een formeel bewijs van 200.000 regels dat ooit 20 mensjaren vergde, kan nu worden gegenereerd in ongeveer twee weken. Dit maakt menselijke expertise niet overbodig — het opstellen van specificaties, het vertalen van veiligheidseisen naar formele logica, blijft een taak die zowel training in formele methoden als diepgaande domeinkennis vereist. Maar bewijsgeneratie is nu voldoende geautomatiseerd om de kostenberekening voor elke veiligheidskritische AI-implementatie te transformeren. Onze methode gebruikt AI-ondersteunde bewijzers om bewijskandidaten te genereren, en verifieert en verfijnt deze vervolgens. Het Lean-Agent Protocol (April 2026) toonde aan dat verificatiecontroles worden uitgevoerd in ongeveer 5 microseconden, snel genoeg voor inline financiële compliance.

Certificeringsnormen zijn in beweging — uw strategie kan niet wachten

Drie regelgevende tijdlijnen komen samen. Van de EU AI Act worden de bepalingen voor hoog risico volledig van kracht op August 2, 2026. ARP6983/ED-324 van SAE G-34/EUROCAE WG-114, de norm voor ML-certificering in de lucht- en ruimtevaart, mikt op June 2026 voor publicatie na 1.800 formele commentaren. ISO/PAS 8800:2024, de eerste norm voor AI-veiligheid in wegvoertuigen, werd gepubliceerd in December 2024, en Geely Auto ontving de eerste wereldwijde certificering hieronder in August 2025.

Elke norm benadert AI-verificatie op een andere manier:

• ARP6983 introduceert het concept van de ML Constituent (MLC) en het Operational Design Domain (ODD).
• ISO/PAS 8800 breidt ISO 26262 en SOTIF uit om zowel functionele veiligheid als risico's van functionele ontoereikendheid in AI te dekken.
• De EU AI Act vereist een conformiteitsbeoordeling maar schrijft geen verificatiemethoden voor, waardoor organisaties passende risicomitigatie moeten aantonen tegen standaarden die CEN/CENELEC JTC 21 nog niet heeft afgerond.

EASA's AI Concept Paper Issue 2 definieert een W-vormig ontwikkelingsproces voor ML-certificering. De eerste verwachte AI-goedkeuring voor Level 2/3A -luchtvaarttoepassingen wordt verwacht voor 2035 — organisaties die bouwen voor lucht- en ruimtevaartcertificering beginnen aan een verificatietraject van een decennium. Wij volgen deze normcommissies en ontwerpen verificatiestrategieën die verdedigbaar zijn onder de huidige conceptversies en aanpasbaar zijn zodra normen worden vastgesteld.

Model checking voor agent-orkestratie

Wanneer uw AI-systeem bestaat uit meerdere agenten die coördineren via gedeelde bronnen, tools aanroepen en sequentiële beslissingen nemen, verschuift de verificatie-uitdaging van neurale netwerkeigenschappen naar protocolcorrectheid. TLA+ -model checking onderzoekt elke bereikbare toestand in uw orkestratieprotocol en bewijst eigenschappen zoals gegarandeerde beëindiging, begrensde herhalingen en delegatielimieten. Z3 SMT-solving vult TLA+ aan door eigenschappen over alle mogelijke inputs te verifiëren: permissie-guards waarvan wiskundig is bewezen dat ze onmogelijk te omzeilen zijn, routingvolledigheid en detectie van race conditions.

Het principe: uw LLM is niet-deterministisch, maar uw orchestrator wel. De deterministische laag kan uitputtend worden geverifieerd. Amazon gebruikte TLA+ om kritieke bugs in DynamoDB, S3 en EBS te vinden die bij testen over het hoofd werden gezien. AgentVerify (April 2026) introduceerde compositionele formele verificatie van multi-agentveiligheid via LTL-model checking. Onze aanpak integreert statische bewijzen voor orkestratielogica met runtime-monitoring voor de stochastische componenten (gedetailleerd beschreven in ons onderzoek naar deterministische waarborgen voor stochastische modellen).

Statische bewijzen verlopen — verificatie moet continu zijn

Formele verificatie veronderstelt dat het geverifieerde systeem ongewijzigd blijft. AI-systemen doen dat niet. Modellen worden hertraind. Prompts veranderen. Tool-bibliotheken breiden uit. Een robuustheidscertificaat afgegeven voor modelversie 1.3 zegt niets over versie 1.4.

Wij ontwerpen verificatie-architecturen die hiermee rekening houden:

• Statische verificatie bewijst eigenschappen van bevroren modelsnapshots — en legt zo de basislijn vast.
• Runtime-verificatie monitort op drift, beleidsschendingen en afwijkend gedrag — en detecteert wanneer de basislijn niet langer standhoudt.
• Wanneer drift drempelwaarden overschrijdt, wordt herverificatie automatisch geactiveerd, waardoor de cyclus wordt gesloten.
• Verificatie-artefacten worden geversioneerd naast modelversies voor volledige controleerbaarheid.

Wanneer formele verificatie de juiste investering is

U heeft formele verificatie nodig wanneer AI-falen gevolgen heeft die testen niet adequaat kan adresseren:

• Verlies van mensenlevens — autonome voertuigen, luchtvaart, medische hulpmiddelen.
• Niet-naleving van regelgeving — EU AI Act hoog risico, DO-178C DAL-A/B, ISO 26262 ASIL-C/D.
• Financiële blootstelling die de verificatiekosten overstijgt — semiconductor respins van $40M+ per iteratie, of algoritmische handel waarbij een enkele schending van een restrictie leidt tot regelgevende maatregelen (zie ons onderzoek naar het realiseren van absolute compliance voor deep AI).

U heeft geen volledige formele verificatie nodig voor aanbevelingssystemen, contentgeneratie, zoekrangschikking of interne analyses. Property-based testing (zoals met QuickCheck/Hypothesis) biedt vaak voldoende zekerheid voor systemen waar onjuiste antwoorden hoogstens ongemakkelijk zijn maar geen directe actie vereisen. Wij beoordelen dit eerlijk voordat we een scope adviseren.

De talentkwestie is cruciaal. Minder dan duizend mensen wereldwijd hebben productie-ervaring in zowel formele methoden als ML-systemen. Deze capaciteit intern opbouwen betekent werven uit een vijver die nauwelijks bestaat; samenwerken met specialisten die beide disciplines al beheersen verkort de tijdlijn van maanden werving naar weken bouwen.

Wat wij leveren

Een traject wordt afgestemd op het leveren van verificatiebewijs dat aansluit op uw regelgevende en operationele vereisten.

• Verificatie van neurale netwerken: robuustheidscertificaten met resultaten van volledige verificateurs (alpha-beta-CROWN, Marabou) voor kritieke deelsystemen, sounde incomplete analyse voor grotere architecturen, en een helder verificatiedekkingsrapport dat documenteert wat volledig is bewezen, wat is bewezen met een sounde overbenadering, en wat empirisch testen vereiste vanwege schaalbaarheidsbeperkingen.
• Agent-orkestratie: TLA+-specificaties met door model checking geverifieerde veiligheidseigenschappen en door Z3 geverifieerde invarianten.
• Certificering: formele specificaties in de notatie die vereist is voor uw doelnorm (temporele logica, eerste-orde logica, Lean 4 of normspecifieke DSL's), gekoppeld aan de conformiteitsbeoordelingseisen van ARP6983, ISO/PAS 8800, ISO 26262 of de EU AI Act voor zover van toepassing.

Een traject levert ook de specificatie zelf op: uw veiligheidseigenschappen en domeininvarianten vertaald naar formele logica. Dit is vaak het meest waardevolle artefact. De bewijstools zullen verbeteren. De normen zullen definitief worden. Uw formele specificaties blijven behouden en sluiten direct aan op compliancedossiers.