---
title: "Harnessing Code Agents for Automatic Software Verification"
source: https://arxiv.org/abs/2607.06341v1
plattform: youtube
channel: cs.AI
duration_seconds: None
thema: Agentic Formal Verification mit Verification-Harness
nutzen: "Liefert das uebertragbare Pattern 'freier Code-Agent + unbestechlicher Accept-Gate' fuer korrektheitsgesicherte Artefakt-Generierung in KADi."
umsetzungsidee: ""
prioritaet: P2
klassifikation: Brain-Entry
confidence: 0.78
status: aktiv
tags: [formal-verification, code-agents, llm, coq, iris, verification-harness, feedback-loop, agentic-se, claude-code, akp, video, auto-ingested]
date: 2026-07-09
akp_run: kar-74
---

# Harnessing Code Agents for Automatic Software Verification

**Channel:** cs.AI · **Dauer:** 0 min · **URL:** https://arxiv.org/abs/2607.06341v1

## Kernaussage
Statt LLMs eine fixe, menschlich vorgegebene Beweisstrategie aufzuzwingen, uebergibt man einem general-purpose Code-Agenten (z.B. Claude Code) das ganze Lemma frei und umgibt ihn mit einem Verifikations-Harness, der Soundness, Vollstaendigkeit und Termination hart erzwingt. Damit werden auf Iris, reglang und iris-lean alle Ziel-Lemmas vollautomatisch bewiesen — 100% Coverage ohne Coq-Experten-Eingriff.

## 7-Punkt Praxisanalyse
### 1. Was koennen wir lernen?
Der Kern-Insight: nicht die Strategie ins Modell verdrahten, sondern dem Agenten Freiheit geben und Korrektheit ueber einen externen Harness mit harten Constraints (accept-only-if-kernel-closes, no dropped obligations, no divergent tactics) sichern. Feedback-Loop + hard gates schlaegt fixed-pipeline. Genau das Muster 'Agent + Verification Harness' ist generalisierbar ueber Formal Verification hinaus.

### 2. Wie koennen wir es einsetzen?
Als Blueprint fuer jeden Aria/KADi-Flow, wo ein Agent Artefakte produziert, die maschinell verifizierbar sind: Code, Configs, Migrations, Proofs. Der Harness = deterministischer Validator, der nur akzeptiert wenn eine formale/testbare Bedingung erfuellt ist; der Agent iteriert unter dessen Feedback frei. Uebertragbar auf CI-Gated-Code-Generation und Self-Healing-Pipelines.

### 3. Konkreter Vorteil fuer Aria / KADi / Supplier Pulse / Workflow / Tools?
Bestaetigt den 'feedback + hard constraints statt vorgeschriebener Micro-Strategie'-Ansatz, den Aria ohnehin verfolgt. Liefert ein sauberes mentales Modell: Agentenfreiheit maximieren, Korrektheit an einem unbestechlichen Gate erzwingen. Verstaerkt die Cross-Ref-Linie (SWE-Doctor, CAPRA) rund um agentisches Software-Engineering unter Feedback.

### 4. Was koennen wir dadurch besser machen?
Paper misst nur Coverage/Pass, nicht Kosten (Token, Wall-Clock, Retries pro Lemma) und nicht Robustheit gegen Harness-Luecken. Ein besserer Ansatz: Harness-Vollstaendigkeit selbst formal beweisen und Cost-Efficiency-Metriken ergaenzen, damit 'volle Coverage' nicht durch unbegrenztes Budget erkauft wird.

### 5. Lohnt sich die Umsetzung — warum?
Ja als Wissensbaustein — das Design-Pattern 'freier Agent + harter Verifikations-Gate' ist direkt auf KADi-Codegenerierung uebertragbar und aendert, wie man Agenten-Guardrails baut. Kein sofortiger Build-Bedarf, aber hoher konzeptioneller ROI.

### 6. Naechste Schritte
1) Brain-Note anlegen und mit SWE-Doctor + CAPRA verlinken (Cluster 'agentic SE under feedback'). 2) Pruefen, ob KADi-Codegen einen expliziten deterministischen Accept-Gate hat statt nur LLM-Self-Check. 3) Optional Spike: 'Verification-Harness-Pattern fuer KADi-Artefakte'.

## Kritik (Pflichtfeld)
Der methodische Kern-Insight (Agent-Freiheit + externer hard-constraint Harness statt fixer Pipeline) ist stark, aber die '100% Coverage / zero failures'-Claims sind mit Vorsicht zu geniessen: ohne Cost-, Retry- und Budget-Zahlen ist unklar, ob das skaliert oder nur mit brute-force-Iteration erkauft ist. Die Benchmarks (Iris-Kernmodule, reglang, iris-lean) sind kuratiert; keine adversariale oder wirklich neuartige Domain. 'Aria proves...' ist hier nur der System-Name des Papers, nicht unsere Aria — potenzielle Verwechslung. Die zugrundeliegende Idee 'LLM + verifier feedback loop' ist zudem nicht voellig neu (verwandt mit prior LLM-provers, RL-from-verifier, self-repair); Neuheit liegt eher im Weglassen der Strategie als in der Loop-Mechanik.

## Multi-Level-Challenge (inline, KAR-72)
**Devils-Advocate:** Das Paper adressiert Coq/Lean-Theorembeweise — ein Nischenfeld, das im KADi/MRR-Alltag praktisch nie vorkommt; der direkte Handlungsbedarf ist null, und das Pattern 'Agent + Validator-Gate' ist bereits generisch bekannt.

**Steel-Man:** Das eigentliche Asset ist nicht Coq, sondern das generalisierbare Architektur-Pattern: Agentenfreiheit + deterministischer hard-constraint Gate ergibt nachweislich hoehere Reliability als vorgeschriebene Strategien — genau das Guardrail-Design, das KADi-Codegen braucht.

**Synthese:** Refine: Als Brain-Note promoten und mit dem agentic-SE-Cluster verlinken, aber ohne Auto-Issue. Falls KADi-Codegen keinen expliziten deterministischen Accept-Gate hat, kann daraus spaeter ein Spike/Issue destilliert werden.

## Adversarial-Critic (separater Call, Cross-Model, KAR-747)
**Verdict:** refine · **Confidence:** 0.72 · **Halluzinations-Risiko:** low

**Urteil:** Analyse ist inhaltlich fair und halluzinationsfrei, aber ueberextrahiert den KADi-Praxisnutzen aus einer Nischen-Formal-Verification-Arbeit und verdient kein Keep ohne Einschraenkung der Uebertragbarkeits-Claims.


**Schwaechen:**
- Namens-Konfusion wird zwar in der Kritik erwaehnt, aber nicht konsequent aufgeloest: 'Aria proves...' im Transcript bezieht sich auf das System des Papers, nicht auf das interne Aria/KADi-Projekt — das haette aus der Analyse komplett herausgehalten oder staerker disambiguiert werden muessen, da es Verwirrung stiftet.
- Der 'Praxisnutzen fuer KADi'-Claim ist generisch-extrapoliert: Das Transcript zeigt ein Formal-Verification-System fuer Coq/Lean-Theorembeweise. Die Uebertragung auf 'CI-Gated-Code-Generation und Self-Healing-Pipelines' ist plausibler Analogieschluss, aber nicht im Transcript begruendet — das ist Uebergeneralisierung.
- Die Kritik an fehlenden Cost/Retry-Zahlen ist korrekt und im Transcript bestaetigt (keine solchen Metriken genannt), aber die Analyse wertet das nur als Limitation, nicht als echtes Signal-Problem: ohne Kostenangaben ist '100% Coverage' potentiell ein unbegrenztes-Budget-Artefakt, was die Uebertragbarkeit fundamental in Frage stellt.
- Confidence 0.78 ist zu hoch angesichts der zentralen Unbekanntheit (Kosten, Skalierbarkeit) und der Nischen-Anwendungsdomaene; 0.65-0.70 waere ehrlicher.
- Das Pattern 'Agent + Verifier Feedback Loop' wird als Kern-Asset verkauft, aber der Novelty-Claim ist im Transcript selbst eingeschraenkt ('existing approaches... prior LLM provers'). Die Analyse haette sauberer abgrenzen muessen, was wirklich neu ist (Weglassen der fixen Strategie) versus was prior art ist (Feedback-Loop selbst).
- Brain-Entry-Klassifikation ist vertretbar, aber angesichts des sehr geringen direkten KADi-Handlungsbedarfs und der Nischen-Domain (Coq-Theorembeweise) koennte 'Ignore' oder zumindest niedrigere Prioritaet als P2 gerechtfertigt sein.

## Cross-Reference (Brain-Match)
- [[2026-05-29-csai-adaptive-multimodal-agents-based-framewo]] (score 95.158)
- [[2026-07-03-csai-swe-doctor-guiding-software-engineering-]] (score 89.677)
- [[2026-06-19-csai-capra-scaling-feedback-on-software-archi]] (score 68.96)

## Klassifikation: **Brain-Entry** · Prioritaet **P2** · Confidence **0.78**

---
*Auto-generated by aria-akp-deep.py · cost $0.2180 · 2026-07-09T04:06:18.410412+00:00*