Technische Samenvatting: Formele Methode-gestuurde Vibe Coding via Model-Driven Engineering

1. Probleemstelling

Het artikel adresseert de kritieke kloof tussen de snelle adoptie van "vibe coding"—een workflow waarbij ontwikkelaars intenties beschrijven in natuurlijke taal aan Large Language Models (LLM's) en gegenereerde code accepteren met minimale controle—en de strikte eisen voor assurance in veiligheidskritische systemen (gereguleerd door standaarden zoals DO-178C, IEC 61508 en ISO 26262).

Huidige benaderingen voor het verifiëren van door LLM's gegenereerde code staan voor twee primaire structurele barrières:

1. Verificatie-bewuste talen: Methoden die zich richten op talen zoals Dafny, Verus of Lean lijden aan een tekort aan pretraining-data voor LLM's, gebrekkige vermogens voor compositioneel redeneren en een gebrek aan integratie met bestaande industriële toolchains (die voornamelijk Java, C of C++ gebruiken).
2. Post-hoc filtering: Bestaande tools die verificatielagen toevoegen na de generatie behandelen verificatie als een filter in plaats van een feedbacksignaal, waardoor er geen mechanisme is om de LLM richting correctheid te sturen.

Gevolg is dat ongestuurde vibe coding artefacten produceert die niet beschikken over de formele correctheidsgaranties en traceerbare bewijslast die vereist zijn voor certificering.

2. Methodologie: De Forge Pipeline

De auteurs presenteren Forge (Formal method Oriented Refinement loop for GEnerated code), een closed-loop pipeline die LLM-generatie integreert met gevestigde Model-Driven Engineering (MDE) infrastructuur. De kernfilosofie is om de LLM te behandelen als een "conceptgenerator" (draft generator) en de MDE-keten als een "discriminator", waardoor ontwikkelaars in mainstream Java kunnen werken terwijl formele verificatie opereert op geëxtraheerde modellen die zij nooit hoeven te zien.

De pipeline bestaat uit zeven fasen gegroepeerd in drie families:

Fase 1: Vereisten Elicitatie

Natuurlijke taalvereisten worden gestructureerd in een formele set van vereisten.

Fase 2: Top-Down Code Synthese (Vibe Coding)

Een LLM (specifiek Anthropic Claude Code) genereert Java-broncode op basis van een vijflaagse prompt-sequentie:

1. Architectuur: Pakket-/class-structuur en mapping van vereisten naar klassen.
2. Skeleton: Compileerbare Java met gestubbed methoden.
3. Leaves: Sensor-, actuator- en operatielogica.
4. Controller: De mode-geneste state machine logica.
5. Review: Zelfrapportage van verzonnen defaults.

Constraints: Om getrouwe modelextractie te waarborgen, wordt de LLM beperkt tot een specifieke Java-subset (bijv. geen lambdas, streams of pattern matching; state machines moeten twee-niveau if-else structuren gebruiken). Deze subset wordt gemotiveerd door de tractabiliteit van modelextractie in plaats van runtime-voorspelbaarheid.

Preflight Checks (2a–2c): De gegenereerde code ondergaat compilatie, checks op de dekking van vereisten-naar-code, en structurele linting tegen de extractieregels.

Fasen 3–5: Extractie en Transformatie

Deze fase zet de Java-broncode om in formele artefacten zonder menselijke tussenkomst:

• Fase 3 (Text-to-Model): Een aangepaste Spoon-to-EMF bridge parseert de Java AST (ondersteunt Java 17+ features zoals sealed interfaces en records) naar een Eclipse Modeling Framework (EMF) model.
• Fase 4 (Model-to-Model): Een Epsilon Transformation Language (ETL) script transformeert het Java EMF-model naar een RoboChart state machine, waarbij modes, transities en guards worden geïdentificeerd.
• Fase 5 (Model-to-Text): Drie onafhankelijke formele artefacten worden gegenereerd:
  1. Dafny Specificaties: Direct gegenereerd vanuit het Java EMF-model voor deductieve verificatie.
  2. CSP-M Scripts: Gegenereerd vanuit het RoboChart-model voor gedragsmatige refinement checking.
  3. Isabelle/HOL Theorieën: Gegenereerd vanuit het RoboChart-model met behulp van Z-Machine notatie voor theorem proving.

Fasen 6–7: Verificatie en Closed-Loop Refinement

• Fase 6 (Verificatie): De drie artefacten worden geverifieerd door hun respectieve tools:
  • Dafny (Z3): Controleert functionele contracten (pre/postcondities, terminatie).
  • FDR4: Controleert gedragseigenschappen (deadlock freedom, divergence freedom) via CSP refinement.
  • Isabelle/HOL: Bewijst structurele invarianten en deadlock freedom over de symbolische transitierelatie.
  • Vacuity Audit (6d): Zorgt ervoor dat bewijzen niet triviaal zijn (bijv. niet slechts true of True).
• Fase 7 (Refinement): Verificatiefouten worden vertaald naar gestructureerde, actiegerichte correctie-prompts (JSON/Markdown). Deze prompts, gekoppeld aan specifieke vereisten en bronregels via een traceerbaarheidsketen, worden teruggevoerd naar de LLM om de code te regenereren. De loop gaat door totdat alle verifieerders slagen of een maximaal aantal iteraties is bereikt.

3. Belangrijkste Bijdragen

1. Closed Draft-and-Discriminate Loop: Een nieuwe architectuur waarbij LLM-gegenereerde mainstream code formeel verifieerbaar wordt gemaakt door deze door MDE-infrastructuur te leiden, waarbij verificatiefouten worden gebruikt als iteratieve correctiesignalen in plaats van post-hoc filters.
2. Spoon-to-EMF Bridge: De eerste EMF-native text-to-model transformatie voor moderne Java (17+), die in staat is om sealed interfaces, records en pattern syntax te verwerken, waarmee een gat wordt gedicht dat is achtergelaten door legacy tools zoals MoDisco.
3. Complementaire Drie-Verifier Design: Een systeem dat Dafny, FDR4 en Isabelle/HOL parallel gebruikt. Het artikel toont aan dat deze verifieerders niet uitwisselbaar zijn; elk vangt verschillende klassen defecten op (bijv. Dafny vangt contractschendingen op, FDR4 vangt gedragsmatige deadlocks op, Isabelle vangt structurele deadlocks in terminal states op).
4. Eind-tot-eind Traceerbaarheid: Een volledig traceerbare keten die natuurlijke taalvereisten koppelt aan gegenereerde bron, tussenliggende modellen en formele bewijzen, wat per-requirement fix-directieven mogelijk maakt.
5. Empirische Validatie: Bewijs dat de loop convergeert naar volledig geverifieerde code over meerdere onafhankelijke runs, specifiek gedreven door verifieerder-feedback.

4. Experimentele Resultaten

De pipeline werd geëvalueerd op drie extern geschreven casestudy's van toenemende complexiteit:

• SRanger: Een enkele controller grondrobot (23 vereisten, ~220 LOC).
• Last Response Engine (LRE): Een AUV safety governor (51 vereisten, ~613 LOC).
• Chemical Detector: Een multi-controller autonome robot (81 vereisten, ~618 LOC).

Belangrijkste bevindingen:

• Convergentie: Over 15 onafhankelijke runs (5 per casestudy) convergeerden alle 15 runs naar volledig geverifieerde code binnen 2 tot 3 iteraties (mediaan 2).
• Noodzaak van Feedback: In een "cold-baseline" experiment (30 runs zonder verifieerder-feedback), convergeerde 0 runs. Single-pass generatie slaagde er niet in geverifieerde code te produceren.
• Rol van Verifieerders: In een "compile-only" ablatiestudie (waarbij verifieerder-feedback verborgen bleef maar compilatiechecks aanwezig waren), produceerden alle 15 runs nog steeds artefacten die bijten op ten minste één formele verifieerder. Dit bevestigt dat de verifieerder-feedback, en niet alleen iteratie of compilatie, convergentie stuurt.
• Defect Detectie: De drie verifieerders vingen verschillende defecten op. Bijvoorbeeld, een structurele deadlock in een terminal mode werd gemist door Dafny en FDR4, maar gevangen door Isabelle, wat een specifieke fix vereiste (het toevoegen van een idle self-loop).
• Kosten: Convergentie nam doorga corner 2–3 iteraties. De wandkloktijd varieerde van ~1 tot 15 minuten per run, gedomineerd door de Isabelle proof tijden wanneer er structurele problemen bestonden.

5. Betekenis en Claims

Het artikel claimt aan te tonen waar formele verificatie structureel moet liggen in een LLM-gestuurde workflow: niet binnen de LLM, en niet als een post-hoc filter, maar als de discriminator in een closed-loop refinement proces.

• Relevantie voor Certificering: De pipeline produceert bewijsvormen die worden erkend door veiligheidsstandaarden (deductieve verificatie, refinement checking en theorem proving), wat een pad biedt naar certificering voor AI-gegenereerde code zonder dat ingenieurs formele talen hoeven te leren of bestaande Java toolchains hoeven te verlaten.
• Haalbaarheid: Het bewijst dat LLM-gegenereerde code in mainstream talen systematisch kan worden getransformeerd naar formele modellen en kan worden geverifieerd, mits er een robuuste extractie- en transformatiepipeline aanwezig is.
• Bescheidenheid: De auteurs stellen expliciet dat dit werk bewijs levert richting een certificeringsgeval, en niet de certificering zelf. Zij erkennen dat volledige certificering extra stappen vereist, waaronder tool-kwalificatie, procesbewijs en onafhankelijke assurance case review, wat toekomstig werk blijft. De bijdrage is de existentie van een levensvatbare pipeline die de verificatieloop sluit.