Technische Samenvatting: Het inzetten van Code Agents voor Automatische Softwareverificatie

Probleemstelling

Formele verificatie biedt de sterkste garanties voor softwarecorrectheid, maar heeft historisch gezien moeite met schalen vanwege de prohibitieve kosten van handmatige bewijsconstructie. Interactieve stellingbewijzers (ITP's) zoals Coq vereisen hoogopgeleide experts om bewijzen stap voor stap samen te stellen, een knelpunt dat wordt verergerd in complexe domeinen zoals separation logic (bijv. Iris), waar concurrency en gedeelde mutable state het bewijzen moeilijk en tijdrovend maken.

Bestaande geautomatiseerde benaderingen proberen dit op te lossen door vaste, door mensen ontworpen bewijsstrategieën in het systeem in te bedden. Deze systemen dwingen Large Language Models (LLM's) doorgaans om specifieke patronen te volgen, zoals het voorspellen van één tactiek per keer, het ophalen van premissen, of het recursief opdelen van doelen. Deze benaderingen lijden echter aan twee kritieke beperkingen:

1. Partiële Dekking: Ze behalen succespercentages van slechts 12%–48% op beschikbare benchmarks.
2. Beperkte Omvang: Benchmarks richten zich vaak op sequentiële programma's of eenvoudige datatypen, waarbij de moeilijke dimensies van concurrency en fijnmazige geheugenredenering, die de uitdagingen van real-world verificatie definiëren, worden weggelaten.

Bovendien vertrouwen deze systemen op "scaffolding"—handmatig ontworde strategieën die dicteren hoe een bewijs wordt opgebouwd. Dit artikel betoogt dat dergelijke scaffolding onnodig en beperkend is, omdat het het volledige gebruik van algemene code-agents verhindert.

Methodologie: Het Aria-systeem

De auteurs stellen Aria voor, een systeem dat een algemene LLM code-agent (specifiek Claude Code draaiend op Claude Opus 4.7) koppelt aan een verificatieharnas. In tegen afwijking van eerder werk legt Aria geen Coq-specifieke bewijsstrategie, premisse-selector of decompositieheuristiek op aan de agent. In plaats daarvan krijgt de agent een volledige lemma en de vrije hand om zijn eigen aanpak te kiezen.

Architectuur

Aria werkt op een drielaagse architectuur:

1. Model Laag: Een stateless LLM-backend die kandidaat-bewijzen genereert op basis van gestructureerde prompts die het huidige doel, de context en feedback bevatten.
2. Agent Laag: Een orchestrator die de sessie beheert, context ophaalt (definities, eerdere lemma's) en modelresponsen interpreteert. Het stuurt de agent niet-interactief aan via een command-line interface.
3. Harnas Laag: De vertrouwensanker. Het omvat de Coq-kernel en handhaaft beleidscontroles. Het dient kandidaat-bewijzen in bij de kernel; als deze worden afgewezen, wordt de foutmelding (mislukte stap, foutmelding, openstaand doel) teruggegeven aan de agent voor revisie.

De Harness Hook Language (HHL)

Een belangrijke bijdrage is HHL, een declaratieve taal die wordt gebruikt om het verificatieharnas te definiëren. HHL stelt engineers in staat om "hooks" te specificeren die worden uitgevoerd vóór of na agent-acties (zoals tool calls zoals Write, Edit, Bash).

• Pre-hooks: Handhaven restricties vóór een actie (bijv. het blokkeren van Admed, het verbieden van nieuwe imports, of het voorkomen van gevaarlijke shell-commando's).
• Post-hooks: Valideren uitkomsten na een actie (bijv. het draaien van de Coq-kernel om het bewijs te verifiëren, het controleren van de dekking van lemma's, of het afdwingen van Iris-coderingsconventies via een linter).
• Retry Loop: Het systeem werkt in een feedback-gestuurde loop. Als het harnas een bewijs afwijst, wordt de fout teruggekoppeld naar de agent, die het bewijs reviseert. Dit gaat door tot maximaal 30 pogingen per lemma.

Belangrijke Operationele Eigenschappen

• Soundness (Correctheid): Alleen bewijzen die door de Coq-kernel worden geaccepteerd, worden als succesvol beschouwd. De kernel fungeert als een onfeilbare oracle; onjuiste outputs kunnen er niet doorheen glippen.
• Completeness (Volledigheid): Het harnas controleert of de doel-lemma daadwerkelijk bewezen is en niet stilletjes is weggelaten of verzwakt (bijv. via Admitted).
• Termination (Terminatie): Een timeout-check voorkomt dat divergerende, niet-terminerende tactieken het systeem laten vastlopen.
• Autonomie: Het systeem draait onbeheerd. Geen menselijke expert grijpt in om tactieken te schrijven, doelen te inspecteren of runs te herstarten.

Experimentele Resultaten

De auteurs hebben Aria geëvalueerd op vier verschillende benchmarks, waarbij ze 100% dekking met nul fouten bereikten en nul expert-interventie over alle instellingen heen.

1. Iris Core (Coq): De primaire benchmark bestaat uit 4.257 lemma's over de vier kernmodules van Iris (algebra, bi, base_logic, program_logic), die de state-of-the-art higher-order concurrent separation logic vertegenwoordigen.
   • Resultaat: Alle 4.257 lemma's bewezen.
   • Efficiëntie: 79,2% op de eerste poging opgelost; gemiddeld aantal retries per lemma was 0,51. Totale modeltijd was ~380 uur.
2. RustBelt (Coq): Verifieerde veiligheidsbewijzen voor de Rust standaardbibliotheek (concurrency en interior mutability types zoals Arc, Mutex, RwLock).
   • Resultaat: Alle 217 lemma's bewezen.
   • Betekenis: Demonstreert dat de aanpak werkt op software die bovenop Iris is gebouwd, niet alleen op de logica zelf.
3. reglang (Coq): Een bibliotheek van regular-language theorie, die voorheen de slechtst presterende benchmark was voor eerdere LLM-provers (Rango bewees slechts ~12,5%).
   • Resultaat: Alle 318 lemma's bewezen.
   • Vergelijking: Eerdere systemen beheerden nauwelijks één op de acht; Aria bewees alles.
4. iris-lean (Lean 4): Een port van Iris naar de Lean 4 prover, gericht op lemma's die nog niet geport of bewezen waren.
   • Resultaat: Alle 72 lemma's bewezen.
   • Betekenis: Toont aan dat de aanpak niet specifiek voor Coq is en werkt met de Lean-kernel.

Modelvergelijking

Het paper vergeleek ook de private Claude Opus 4.7 met open-source modellen (Kimi K2.6, DeepSeek V4 Pro). Hoewel open-source modellen eenvoudigere lemma's konden bewijzen, hadden zij moeite met lange, complexe bewijzen (bijv. >50 regels) en raakten ze vaak hun retry-budget kwijt. Het private model construeerde betrouwbaar bewijzen van meer dan 200 regels.

Belangrijkste Bijdragen

1. Harnas + Code Agent Paradigma: Het paper demonstreert dat een algemene code-agent, gekoppeld aan een verificatieharnas en vrij om zijn eigen strategie te kiezen, beter presteert dan systemen met hard-wired bewijsstrategieën. Het bereikt volledige dekking op de moeilijkste separation logic bewijzen, een prestatie die voorheen onbereikbaar was.
2. Iris en RustBelt Verificatie: Dit is het eerste empirische bewijs dat een state-of-the-art LLM volledig en automatisch een expert-grade, state-of-the-art softwareverificatiebibliotheek (Iris) en haar downstream toepassingen (RustBelt) kan bewijzen.
3. HHL (Harness Hook Language): Een declaratieve taal voor het definiëren van herbruikbare, auditeerbare verificatiebeleid rondom LLM-agents, waarbij de redenering van de agent wordt gescheiden van de correctheidsgaranties.

Betekenis en Claims

Het paper concludeert dat de "scaffolding" van vaste bewijsstrategieën onnodig is. Door de volledige lemma aan een capabele agent te geven en een harnas te gebruiken om soundness, completeness en termination af te dwingen, kan het systeem de complexe zoekruimte van formele bewijzen autonoom navigeren.

De auteurs claimen dat deze aanpak niet alleen de handmatige bewijs-bottleneck voor Iris wegneemt, maar voor de gehele body van software die erop gebouwd is. De resultaten suggereren dat huidige state-of-the-art modellen in staat zijn om bewijzen voor state-of-the-art geverifieerde softwareontwikkeling volledig en automatisch te schrijven, mits zij worden geleid door een rigoureuze verificatieloop in plaats van een beperkte, door mensen ontworpen strategie. Het paper claimt niet de specificatiegeneratie op te lossen, maar focust strikt op de bewijs-synthese fase.