Paper deep dive

Harnessing Code Agents for Automatic Software Verification

Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Year: 2026Venue: arXiv preprintArea: cs.FLType: PreprintEmbeddings: 72

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%

Last extracted: 7/8/2026, 5:43:47 AM

Summary

The paper introduces Aria, an automated software verification system that pairs a general-purpose LLM code agent (e.g., Claude Code) with a strict verification harness. Unlike prior approaches that enforce fixed, human-designed proof strategies, Aria allows the agent to autonomously generate and revise complete proofs under kernel-level constraints. Evaluated on complex benchmarks like Iris, RustBelt, reglang, and iris-lean, Aria achieves 100% proof coverage without human expert intervention, demonstrating that state-of-the-art LLMs can fully automate expert-grade formal verification.

Entities (16)

Iris · framework · 99%Aria · system · 98%Coq · theorem-prover · 98%Claude Code · software · 97%Separation Logic · concept · 97%Claude Opus 4.7 · llm-model · 96%Verification Harness · component · 96%HHL · language · 95%Lean 4 · theorem-prover · 95%RustBelt · verification-project · 94%reglang · benchmark · 93%COPRA · prior-system · 90%PALM · prior-system · 90%Rango · prior-system · 90%CoqGym · dataset · 88%CoqStoq · dataset · 88%

Relation Signals (18)

Aria → achievescoverage → Iris

confidence 98% · Aria proves all 4,257 lemmas of the four core modules

Aria → targets → Iris

confidence 98% · Its main target is the Iris development

Iris → implements → Separation Logic

confidence 97% · Iris is a framework for proving that concurrent, memory-manipulating programs meet their specifications. It is the modern realization of separation logic

Aria → utilizes → Claude Code

confidence 97% · handing the whole lemma to a general LLM code agent—for example, Claude Code

Aria → achievescoverage → RustBelt

confidence 96% · Aria successfully proves all 217 lemmas

Verification Harness → enforces → Correctness

confidence 96% · the harness checks each attempt and... returns precise feedback

Aria → targets → Coq

confidence 96% · Aria proves all 4,257 lemmas in Iris’s four core modules... in Coq

Aria → achievescoverage → reglang

confidence 95% · Aria successfully proves them all

Iris → implementedin →

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

70,326 characters extracted from source content.

Expand or collapse full text

Harnessing Code Agents for Automatic Software Verification Shuangxiang Kan Shuanglong Kan Sebastian Ertel Abstract Formal verification offers the strongest available guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically. Existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it—retrieving relevant premises and predicting tactics one step at a time, or recursively splitting a goal into subgoals by divide-and-conquer—yet still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary, and limiting: handing the whole lemma to a general LLM code agent—for example, Claude Code [2]—free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving surprisingly full coverage—every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs with effective feedback and hard constraints from the harness that keep each one sound (accepted only when the prover’s kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent, non-terminating tactics). We evaluate the harness + code agent for verified software development along three dimensions. (1) Core logic for software verification: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust’s standard libraries (Arc, Mutex, RwLock, RefCell) built on it—both in full and fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior LLM provers manage barely one in eight, Aria proves all 318. (3) Generality across provers: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. We conclude that a state-of-the-art model—Claude Opus 4.7—is capable of writing proofs for state-of-the-art verified software development fully and automatically. I Introduction Software defects cost the global economy trillions of dollars each year, and the systems where a single bug is most catastrophic—compilers, operating-system kernels, cryptographic libraries—are precisely the ones that most need strong correctness guarantees. Formal verification provides the strongest such guarantee available: a machine-checked proof, constructed in an interactive theorem prover (ITP) such as Coq [55, 4] or Isabelle [45], that a program meets its specification. Landmark efforts such as the CompCert verified compiler (developed roughly 20 years as of 2026) demonstrate that this level of assurance is attainable in practice. Yet verified software remains the exception rather than the rule, for one stubborn reason: the proofs must be written by hand. The obstacle is the cost of those proofs. Constructing an ITP proof requires a highly trained expert to compose tactics one step at a time, reasoning simultaneously about the program, its specification, and the prover’s underlying type theory. Nowhere is this harder than in separation logic [46] and its modern realization, Iris [30, 32], where concurrency, higher-order state, and ghost resources—auxiliary, proof-only bookkeeping, invisible to the running program, that tracks how shared state is allowed to evolve—can make a single lemma take an expert hours or even days to discharge. This manual-proof bottleneck—more than any limitation of the underlying theory—is what keeps verified software from scaling to everyday engineering practice. A growing body of work attacks this bottleneck with machine learning. Early systems learned to predict Coq tactics from corpora of human proofs and drove a search over the proof tree [64, 52, 6, 5]. Large language models (LLMs) then shifted the paradigm toward generating whole proofs or large fragments, augmented with premise retrieval and feedback-driven repair, with strong results across Isabelle [19, 28], Lean [65, 63], Metamath [47], and Coq [41, 61, 56]. Two limitations recur across this prior work, summarized for the Coq systems in Table I. First, although these systems are automatic, their coverage is partial: reported success rates span roughly 12%–48% of the theorems attempted—PALM proves 40.4% of 10,842 CoqGym theorems [41], Rango 32.0% of 10,396 CoqStoq theorems [61], and the strongest LLM agent, COPRA, 48.3% of a small 118-theorem CompCert subset [56]. Second—and more telling—this partial coverage is measured on the easy part of the problem. The benchmarks are drawn from real Coq developments but consist almost entirely of sequential program and datatype verification; they omit the two dimensions that make real-world software verification hard: concurrency and fine-grained reasoning about shared, mutable memory—exactly what separation logic exists to handle. CompCert is a sequential C compiler, and CoqGym and CoqStoq aggregate open-source projects with little concurrent or heap-intensive code. The higher-order, concurrent separation logic that Iris embodies—where interacting threads and the shared state they manipulate make proofs dramatically harder—is left untouched. TABLE I: Learning- and LLM-based automated proof systems for Coq. System Year Benchmark Theorems Proved ASTactic [64] 2019 CoqGym 13,137 12.2%‡ Proverbot9001 [52] 2020 CompCert 501 19.4%‡ Graph2Tac [5] 2024 Coq Opam pkgs 2,000§ 26.1%§ PALM [41] 2024 CoqGym 10,842 40.4% COPRA [56] 2024 CompCert† 118 48.3% Rango [61] 2025 CoqStoq 10,396 32.0% Cobblestone [33] 2026 CoqGym 100¶ 48% ProofCoop [34] 2026 CoqGym ∼ 11.9K 33.0%‡ †118-theorem subset of CompCert (501). ‡Learned model alone, no hammer/solver. §Random 2,000-theorem sample; 33.2%33.2\% with a k-N solver. ¶One of four 100-theorem subsets; 5555–58%58\% with oracle guidance. Despite their variety, these systems share a commitment: each wraps the model in a hand-engineered strategy that dictates how a proof is built. One family works tactic by tactic, searching the proof tree—a trained tactic predictor [64, 52, 6, 5], an in-context LLM with backtracking [56], or retrieval-augmented step prediction [61]. Another generates a whole proof and wraps it in an engineered loop—symbolic repair with backtracking [41], or divide-and-conquer over subgoals [33]. Either way, a fixed, human-designed procedure governs the construction. This paper shows that the scaffolding is unnecessary: general code agents such as Claude Code and Codex can replace it with better results. In confining the model to a narrow role—predict a tactic, or fill a slot in a repair loop—prior systems never tap the power of such an agent: one that reads the context, decides what to do next, and builds the proof however it sees fit. Our method is deliberately coarse: we hand a whole lemma to a general LLM code agent—an off-the-shelf coding tool built for everyday software engineering, here Claude Code on Claude Opus 4.7, not specialized for Coq or theorem proving—and let it write a complete proof however it sees fit. We drive the agent non-interactively through Claude Code’s claude -p command, which embeds in an ordinary program (a Python driver, in our case), so the whole campaign runs automatically with no human at the keyboard. The agent is free to err: a verification harness built on the Coq kernel checks each attempt and, on rejection, returns precise feedback (the failing step and the open goal); the agent revises and retries the whole proof, up to thirty times, until the kernel accepts it. We impose no premise selector, tactic-level search, decomposition, or repair procedure—only the verifier and a thin policy around it. Surprisingly, this is enough, and not merely on easy benchmarks: it reaches full coverage on the hardest separation-logic proofs in existence. Two properties of interactive theorem proving make it work. Trust is free: the kernel rejects anything incorrect, so the confident-but-wrong output that makes LLMs risky elsewhere [26] cannot slip through—the difficulty is never whether to believe a proof, only whether the model can find one, a long, exact, multi-step construction in which a single wrong step is fatal. And the harness closes the loop: rather than produce a correct proof in one shot, the agent proposes a candidate, reads the exact error, and revises, turning proof construction into a guided search against ground truth that a capable agent can direct on its own. We realize this idea as Aria. To make the harness reusable, we express it in a declarative language, the Harness Hook Language (HHL), written against a general code-agent interface so that the same harness can drive different code agents, such as Claude Code and Codex; in this paper it targets the Claude Code SDK [2]. A harness written in HHL bundles the checks that surround the agent for proof writing: a timeout check for divergent, non-terminating tactics; a hallucination check that rejects proofs closed with Admitted or with target lemmas silently dropped; an Iris linter; and final Coq kernel verification. Each lemma runs in a single autonomous session—the agent attempts a proof, the harness checks it, and on failure the agent retries on the returned feedback—with no human in the loop. We evaluate Aria on four bodies of proofs—three in Coq and one in Lean. Its main target is the Iris development [31, 36]—the state-of-the-art separation logic for verifying concurrent, memory-manipulating programs, and arguably the most demanding such proofs in existence, a real, curated artifact rather than a synthetic benchmark. Aria proves all 4,257 lemmas in Iris’s four core modules (algebra, bi, base_logic, program_logic) fully automatically, with zero expert intervention and zero failures. Three further settings then test whether this result holds beyond the Iris core. The first is the verified software built on Iris: the RustBelt safety proofs [29] for Rust’s standard libraries—its concurrency and interior-mutability types such as Arc, Rc and Weak, Mutex and RwLock, RefCell, and Cell; Aria successfully proves all 217 lemmas. The second is a direct comparison with prior work on its own terms: reglang, a 318-theorem library of regular-language theory. Far less demanding than the Iris core, reglang is nonetheless the CoqStoq benchmark on which prior LLM provers fare worst, proving barely one in eight [61]; Aria successfully proves them all. The third moves to a different prover entirely: iris-lean, the in-progress Lean 4 port of Iris, where we target lemmas not yet ported, and Aria proves all 72. Aria is complete across all four settings. This paper makes the following contributions: • Harness + code agent. We propose pairing a general-purpose LLM code agent with a verification harness, imposing no Coq-specific proof strategy, and show that this simple design surprisingly achieves full coverage—every targeted lemma proved, with no failures and no Coq expert intervention. • Evaluation on Iris and its Rust applications. We evaluate the approach on Iris, the state-of-the-art higher-order concurrent separation logic, together with the Rust library verification built on it, proving both completely. This is, to our knowledge, the first empirical evidence that a current state-of-the-art LLM can write the proofs of an expert-grade, state-of-the-art software-verification Coq library. • HHL: a language for writing harnesses around LLM agents. We introduce HHL, a declarative language that makes the harness a reusable, auditable artifact—written once and applied across lemmas, libraries, and agent backends—rather than ad-hoc glue code. The rest of the paper covers the Iris framework (Section I), Aria’s architecture (Section I) and the HHL language (Section IV), its implementation (Section V), the evaluation (Section VI), and discussion and related work (Sections VII and VIII). I The Iris Separation Logic Framework In this section we introduce Iris, the primary benchmark of this work. The premise that motivates the whole paper is this: if an automated system can master proofs as hard as Iris’s, then—because so much software verification is built on Iris—it removes the manual-proof bottleneck not for Iris alone but across that whole body of software, letting verified software development scale to everyday engineering practice. The rest of this section makes the case for that premise: we sketch what Iris is and how it grew, survey the verified software built on it, and explain why its proofs are so hard—the difficulty that motivates automating them. Iris [30, 32] is a framework for proving that concurrent, memory-manipulating programs meet their specifications. It is the modern realization of separation logic [46], whose central idea—reasoning about disjoint regions of memory independently—makes verification of pointer-heavy code tractable. Developed at MPI-SWS and Aarhus University and first released in 2015, Iris has been refined for more than a decade into a large, actively maintained Coq library, extending separation logic to handle the features pervasive in real-world software: concurrency, higher-order functions, and the fine-grained sharing of mutable memory. Iris is not a single-purpose tool but the substrate beneath a broad and growing body of verified software. Its best-known application is RustBelt [29], the first formal safety proof for the core of Rust, showing that Rust’s type system safely encapsulates the unsafe code in its standard library. Beyond it, Iris underpins verified work across many domains: programming-language safety (RustHornBelt [42], RefinedRust [21], Rust under relaxed memory [15], Iris-Wasm [48]); systems software such as C verification (RefinedC [50], Quiver [54]), crash-safe storage in Go (Perennial [9], GoJournal [10], DaisyNFS [11]), and hypervisors [40]; distributed and concurrent systems (Aneris [38], Grove [53], Trillium [62], Actris [25], Hazel [16], Cosmo [43], Zoo [1]); compilers and machine code (Simuliris [22], Islaris [49], Cerise [23], Melocoton [24], DimSum [51]); and security (SeLoC [20], Cryptis [3]). This breadth places Iris at the heart of modern verified software development: it sits under programming languages, compilers, distributed systems, and machine code alike. That reach comes at a cost. Iris proofs are among the hardest in all of software verification: a single non-trivial lemma can take an expert hours or even days, because the proof must account for every way concurrent threads can interleave and share state, with little syntactic guidance on what step to take next [36, 31]. Because Iris demands such deep understanding, developing verified software on top of it requires experts who have that understanding—a bottleneck that keeps verified software from scaling. That is what makes the premise above worth testing: automate proofs this hard, and the bottleneck eases for the broad range of software built on Iris. I Architecture The Aria system, our system for proving Coq lemmas fully automatically with a code agent, is organized as a three-layer architecture: the model layer, the agent layer, and the harness layer. This separation cleanly decouples the non-deterministic reasoning capabilities of the LLM from the deterministic correctness guarantees of the proof assistant. Figure 1 illustrates the overall structure and the information flow between layers. Model LayerLLM backend (stateless inference)Agent Layerorchestration, context assemblyHarness LayerCoq kernel ++ policy hooks; feedback & retrypromptcandidateprooferror Figure 1: Three-layer architecture of Aria. I-A Model Layer The model layer is the source of proof candidates. It consists of one or more LLMs—for example, proprietary models from Anthropic, Google Gemini, and OpenAI, or open-source models such as Llama, Qwen, and DeepSeek—accessed through a uniform inference interface that treats each model as an interchangeable backend. Given a structured prompt that encodes the current proof obligation together with the surrounding context and any prior feedback, the model generates a candidate proof and writes it into the source file at the appropriate location. I-B Agent Layer The agent layer is the orchestrator and the locus of intelligence beyond raw model inference. It owns both proof construction and strategy: choosing which lemma to attack and how to approach it—retrieving similar proofs, definitions, dependencies, and prior lemmas as context—then prompting the model and interpreting its response into a candidate proof. When the harness returns an error and the pending goals of a proof, the agent revises accordingly; the retry loop itself is driven by the harness layer below. The agent layer also enforces the session-scoping policy, ensuring that context remains focused and token usage bounded. The agent layer is not tied to a particular code agent: any runtime that exposes the interfaces our harness relies on—tool dispatch and the pre-/post-tool and turn-level hooks through which policy is enforced—can serve as the agent layer, whether Claude Code, Codex, or another coding agent. I-C Harness Layer The harness layer is the trust anchor of the system. At its core it wraps the Coq proof assistant as a verification oracle, but it also runs the auxiliary policy checks that surround it—a per-tactic timeout for divergent tactics, a ban on admit/Admitted (which indicate dropped proofs), a lemma-coverage check, an Iris linter, and shell-command safety. Every candidate the agent produces must pass through the harness before it counts as successful: the harness submits the proof to Coq and, on rejection, returns a structured report—the failing step, the error message, and the pending goal—and drives the feedback loop, handing that report back to the agent and re-dispatching until a proof is accepted or the retry budget is exhausted. The harness does more than judge correctness. Correctness is decided by the Coq kernel, not the model or the agent, so no unverified proof can leave the system. Beyond that, the harness governs style, holding each proof to Iris’s conventions, and safety, blocking unwanted or destructive shell commands. This makes the harness the foundation upon which the entire LLM + Harness paradigm rests. IV The Harness Hook Language (HHL) A central design choice of Aria is to expose the harness layer through a dedicated, declarative language rather than as an ad-hoc library of glue code. We call this language HHL. HHL is the surface through which proof engineers describe how the LLM should be driven, what actions it is allowed to take, and which verification steps must succeed before a proof is accepted. By making these concerns first-class language constructs, HHL keeps the agent layer concise and auditable while letting the harness layer enforce strong correctness guarantees uniformly across all proof attempts. IV-A Overview by Example Figure 2: An example HHL program. ⬇ hook check_imports: Write|Edit(file, original) = check_imports_fn hook no_banned: Write|Edit(file, original) = no_banned_fn hook safe_command: Bash(cmd) = safe_command_fn hook iris_lint: Turn(files) = iris_lint_fn hook verify_proof: Turn(files) = verify_proof_fn workspace coq_project cwd = "/path/to/project" system_prompt = "You are an Iris expert ..." allowed_tools = ["Read", "Bash", "Write", "Edit"] max_turns = 10 workflow prove_lemmas(lemmas: list[string]) for lemma in lemmas var proved = false var tries = 0 var feedback = "" while !proved && tries < 30 let r = invoke(coq_project, "Prove the lemma " ++ lemma ++ feedback, pre:[check_imports,no_banned,safe_command], post:[iris_lint, verify_proof]) proved = !r.is_error feedback = " error: " ++ r.result tries = tries + 1 if proved print("Proved: " ++ lemma) else print("Failed: " ++ lemma) We introduce HHL by walking through the example program in Figure 2 (a simplified version of Aria), whose prove_lemmas workflow proves a list of Iris lemmas under a policy of five hooks. An HHL program begins with its hook declarations: each binds a tool event to a Python policy function that runs around the corresponding agent action, bracketing it: pre-hooks ⟶\; \; agent action ⟶\; \; post-hooks They fire in list order: each pre-hook runs (and may block the action) before it, left to right, and each post-hook runs after it, in turn. Each declaration, hook name: Event(payload) = fn, binds a Python function to a tool event. A pre-hook such as hook no_banned: Write|Edit(file, original) = no_banned_fn fires before a Write or Edit tool call, inspects the payload (here the file being written and its original contents, from which it can compute the edit’s diff) and returns Allow or Deny to permit or block it—here denying the edit whenever its diff introduces a banned construct such as admit or Admitted, or anything else the policy forbids, such as an Axiom that assumes the goal outright. A post-hook instead runs after a tool call—or, for the Turn event, at the end of a turn (one round of model output and the tool calls it triggers)—and returns Ok or Err to accept or reject the attempt; verify_proof, for example, type-checks the edited file with the Coq kernel, which can only be done once the edits are in place. Besides no_banned above, the two remaining pre-hooks are: • check_imports — rejects any edit that adds a new Require or Import, so a proof may use only the modules already in scope; for our experiments, the existing imports are sufficient; • safe_command — screens shell commands, blocking build and file-deleting (rm) commands. Build and verification commands are blocked for two reasons: the harness already type-checks each turn, so the agent never needs to build itself; and a mis-issued build—most likely when the model guesses at flags or targets—scatters stale compiled artifacts (.vo, .vos, .glob) across the tree, corrupting the project’s incremental build state and derailing every later attempt; recovering would then require a human to clear those files, breaking the otherwise unattended run. The two Turn post-hooks run once the turn completes. verify_proof is the one described above; besides type-checking with the Coq kernel, it also runs a coverage check that no target lemma was dropped or altered. The other, iris_lint, enforces Iris’s coding conventions; we place it as a post-hook rather than a pre-hook so the LLM can first concentrate on finding a working proof, with the linter applied afterward to polish it into Iris’s conventions. To see these hooks in action, consider proving a lemma in Iris. For it, the prove_lemmas workflow issues an invoke, the primitive that runs one model interaction. As Figure 2 shows, invoke takes four arguments: the coq_project workspace (the run environment—working directory, model, system prompt, and allowed tools), a prompt, and the lists of pre- and post-hooks. Here the prompt merely names the target ("Prove the lemma " ++ lemma)—not its statement; the agent reads the source file to recover the statement and the definitions and prior lemmas in scope, then writes a proof into the file as a sequence of Coq tactics. Each write is gated by the pre-hooks, and when the turn ends the Turn post-hooks run; if every hook passes, invoke returns success and the workflow records the lemma as proved, otherwise it returns the verifier’s error. The workflow wraps invoke in a feedback-driven retry loop, written in Figure 2 as a while over three var bindings: proved (set from !r.is_error), a tries counter, and feedback, the verifier’s error read from r.result. On rejection, feedback is appended to the next invoke’s prompt, so the agent sees what went wrong and revises; the loop condition !proved && tries < 30 keeps retrying until a proof is accepted or the thirtieth attempt, after which the lemma is recorded as failed. Aria additionally resumes the same session across retries, carrying the full error history forward. IV-B Syntax and Compilation An HHL program declares hooks that bind a tool event to a Python policy function, workspaces that fix the run environment, embedded Python, and one or more workflows; execution starts from a designated entry-point workflow. A workflow orchestrates with ordinary control flow (let/var, if, while, for, match), may call other workflows, and drives the model through the invoke primitive, which runs one model interaction under chosen pre-/post-hooks and returns a Response the workflow branches on (is_error, result). Each hook receives the event payload—a File, EditOp, or Command—and returns Allow/Deny for pre-hooks or Ok/Err for post-hooks; its body is ordinary Python, so it can grep a file, call an external checker, or shell out to the prover. HHL is compiled, not interpreted: the compiler resolves require dependencies and lowers the program to Python on a target agent runtime—currently the Claude Code SDK [2], though, because it depends only on tool dispatch and pre-/post-tool hook points, it can be retargeted (e.g. to the OpenAI Agents SDK) without changing any hook or workflow. Table I gives the mapping: each hook becomes a Python script wired into the SDK’s PreToolUse/PostToolUse protocol through a generated settings file (a Turn hook, having no native counterpart, becomes post-turn logic in the driver), the workspace becomes the run configuration, and each invoke becomes one claude -p run—a non-interactive (headless) shell command, so the whole workflow executes as a program with no human at the keyboard. TABLE I: How the HHL compiler lowers each construct. HHL construct Claude Code SDK target pre hook on Write/Edit PreToolUse (Write|Edit) pre hook on Bash PreToolUse (Bash) post hook on Write/Edit PostToolUse (Write|Edit) post hook on Turn driver post-turn logic workspace run configuration invoke a claude -p run V Aria Implementation Aria runs as a single, long-lived campaign. Once launched on the four core Iris modules, it proves all 4,257 lemmas autonomously—discovering the targets, generating and repairing proofs, keeping the project in a buildable state, and logging every outcome—with no human expert in the loop: from launch to the last completed proof, nobody inspects a goal, writes a tactic, or restarts the run by hand. The campaign we report ran for roughly 380 hours of model time (about 16 days); the only human action it required was starting it. Under the hood, Aria runs as a small team of specialized LLM agents, coordinated by a driver program and kept honest by automatic checkers (Figure 3). The driver runs the whole campaign. It first uses an Extractor simply to find which lemmas still need a proof; a quick completeness check (the extraction harness in Figure 3) confirms that none were missed. The driver then gives each lemma to a Prover, which writes a first proof attempt and submits it to the Coq harness. If the harness rejects it, the error message and the still-open goal are handed to a Fixer, which revises the proof and resubmits—looping, always with the latest error and goal in hand, until the harness accepts the proof or an attempt limit is reached. A Polish agent then rewrites the accepted proof toward the style rubric, with the harness re-checking each rewrite. The model is never taken at its word: a lemma counts as proved only once the Coq harness has checked it. Driver (HHL workflow)orchestrates the campaignExtractorunproved→ lemma namesProverfirst attemptFixerrepairs on error(retry ≤30≤ 30)Extractionharnesslemma-count checkCoq Harness (kernel ++ hooks)verify_proof, iris_lint, no_admitted,safe_command, timeoutPolishrubric style (retry ≤2≤ 2)extract / nameslemmavalidateprooferror++goalfixed proofacceptedre-check Figure 3: Aria’s multi-agent proof loop. Each LLM role (Extractor, Prover, Fixer, Polish) is paired with a harness that validates its output. V-A Critical Harness Design The verification harness is the core of Aria and its only source of trust. Two checks turn each rejection into usable feedback: a Coq verification check that pins an error to a line and goal, and a divergent-tactic check that catches proofs that never terminate. V-A1 Coq verification After each turn the harness takes the single .v file the agent has just modified and checks it with Coq, one proof step at a time. If the file compiles cleanly, the turn is accepted. If a step fails, the harness stops at that point and returns three things: the line where the proof broke, Coq’s error message, and the pending goal at that line—the proof state Coq was in when the tactic failed, recovered by replaying the proof up to the failing step. This is what turns a rejection into usable feedback. A bare “the proof failed” tells the model nothing; an error pinned to a line, together with the goal that still has to be proved, tells it exactly where it went wrong and what remains. For instance, on an attempted proof of P∧Q→Q∧P Q→ Q P whose last step wrongly applies the hypothesis HP : P to the goal Q, the harness reports: ⬇ (1) failing step (line 4): apply HP. (2) error message: Unable to unify "P" with "Q". (3) pending goal: HP : P, HQ : Q ---------------- Q The model now knows the offending tactic and the goal it must discharge, and can revise accordingly. V-A2 Divergent-tactic check Some tactics diverge—they neither succeed nor fail, but run forever, as when a heavy automation tactic searches without end or a repeat loops without making progress. Coq itself never comes back—there is no error to catch, only a hang—so the harness caps each tactic at 300 s: when a step exceeds that, the harness stops it and reports a timeout at the stuck step, together with the pending goal just before that tactic. This both tells the model the step is too expensive to use and keeps one divergent attempt from stalling the whole campaign. V-B Session (Context) Management The proof loop is driven by a conversational session with the model, and how that session is reused is central to Aria’s effectiveness. The workflow asks the model to prove each lemma and submits the file to the harness, retrying up to 30 times on rejection, each time feeding back the error and the pending goal. The retries are not independent: each retry resumes the same session, so the model keeps the entire conversation—its earlier attempts and the accumulated chain of errors and goals—and builds on what it has already tried instead of repeating dead ends. The Polish agent, by contrast, runs in its own fresh session, sharing none of the Prover’s or Fixer’s history: polishing starts from the accepted proof alone, keeping it independent of—and a fair check on—the proof-finding effort. Sessions are reused across lemmas as well, but only briefly—a deliberate tradeoff. Within a file, a session carries over at most six consecutive lemmas before it is reset, and every new file begins fresh. Reuse helps because adjacent lemmas in an Iris file tend to share definitions and proof ideas, so the model can carry over tactics it has just found; the window of six is a rule of thumb that assumes such nearby lemmas are related. Push the reuse further, though, and the session accumulates a long history that dilutes the relevant context and slows the model down, making it less likely to land a proof quickly. Resetting costs little: a fresh session can always re-read whatever it needs from the source file, so it loses the conversation, not the information. VI Experiment Our implementation of the agents is available in an anonymized repository: https://anonymous.4open.science/r/CoqProver-Code-57B. The experiments were conducted on a Claude Code 20× subscription rather than the metered API, which significantly reduced cost. VI-A Experimental Setup Benchmarks. We evaluate Aria on four independent bodies of proofs—three in Coq and one in Lean. The primary target is the Iris core—the four core modules of the Iris Coq development [57], comprising every lemma whose original, expert-written proof terminates in Qed: 4,257 lemmas across 113 files. We deliberately include the entire population rather than a sample, so our results characterize the complete modules. To test whether the approach carries beyond the Iris core, we add three further benchmarks: the Rust library Coq verification in the RustBelt project [60] (217 lemmas); reglang, a Coq library of regular-language theory [17] that is the CoqStoq project on which prior LLM provers fare worst [61]; and iris-lean [58], three not-yet-ported files of the in-progress Lean 4 port of Iris (72 lemmas), whose proofs are checked by the Lean kernel rather than Coq’s. Proof-regeneration protocol. For each target lemma we remove its original proof body, leaving the lemma statement intact, and task the agent with reconstructing a proof from scratch. The remainder of the source file—surrounding definitions and notations—together with all imported dependencies remains available as context; only the proof under test is removed. Resource restrictions. So the agent reconstructs each proof rather than retrieving it, we run it in a sandbox with no network and no version control: it can neither browse the web nor recover the removed proofs from git history. Its only resources are the on-disk .v files—with the target proofs removed—and the dependent libraries installed via opam. Any proof it produces is therefore built from the lemma statement and its in-scope context, not copied from the reference proof. Models. Unless stated otherwise, all results use a single backend—Claude Opus 4.7—with no other model involved. Aria’s model layer is nonetheless backend-agnostic. We examine how the choice of model affects the outcome separately in Section VI-G. Metrics. For each lemma we record whether it was proved, the number of retries it took, and the time to that proof. The reported time is model time—the wall-clock time the LLM spends reasoning and generating the proof. A retry is one in-session repair the agent makes after the harness rejects a candidate, so a lemma’s retry count is its number of failed attempts and a first-attempt success is a retry count of zero. The agent retries up to a cap of 30 per lemma; if the cap is reached without an accepted proof, the lemma is recorded as a failure. VI-B Iris Core The four core modules of Iris, from most abstract to most concrete: (1) algebra defines the resource structures that track ownership; (2) bi defines the logic’s connectives, such as the separating conjunction; (3) base_logic adds invariants and other mechanisms for shared state; and (4) program_logic adds the rules relating code to its specification. Table I summarizes the outcome of running Aria over the Iris Coq development. Aria proved 4,257 distinct lemmas across 113 source files with zero Coq expert intervention and no failures. The vast majority of lemmas—79.2% (3,373 of 4,257)—were solved on the agent’s first attempt, with no retry needed, and the mean retry count per lemma was only 0.51, indicating that the LLM + harness loop converges quickly for the overwhelming majority of proof obligations. This high first-attempt rate is not a sign of memorization: apart from trivial one-line lemmas, whose proof is essentially forced, the proofs Aria generates differ from the upstream Iris proofs—it constructs them rather than recalling them. The most any lemma required was 28 retries—below the cap of 30—so no lemma ever exhausted the retry budget, consistent with the absence of failures. The full run consumed roughly 380 hours of model compute, averaging 321 seconds per lemma; per-lemma cost ranged from a few seconds for simple structural lemmas to over 4.7 hours for the single most demanding obligation. Figure 4 breaks these results down by module. The profile is uniform across all four: every module is solved completely, with first-attempt rates between 7272 and 87%87\% and well under one retry per lemma on average. The algebra module—the resource-algebra layer—is the most demanding, with the lowest first-attempt rate (71.9%71.9\%) and the highest mean retries and time per lemma, while the more derivative bi and base_logic layers converge fastest. Notably, retries and time do not track each other: in Figure 4, program_logic has the fewest maximum retries (11) yet nearly the highest mean time per lemma, whereas bi has the most (28) yet the lowest mean time. This indicates that the reasoning time of each attempt varies with the logical complexity of the lemma, independent of the number of retries. TABLE I: Aria results on the core modules of the Iris Coq development (distinct lemmas, duplicate re-runs removed). Metric Value Distinct lemmas proved 4,257 Source files covered 113 Failures 0 First-try success (0 retries) 3,373 (79.2%) Mean retries per lemma 0.51 Total model time 379.7 h (15.8 d) Mean time per lemma 321.1 s Min / max time per lemma 8.7 s / 17,103 s algebrabibaseprog0202040406060808010010071.971.984.384.387.387.375.875.8First-attempt (%)algebrabibaseprog00.20.20.40.40.60.60.80.80.730.730.350.350.310.310.550.55Mean retriesalgebrabibaseprog01010202030302121282815151111Max retriesalgebrabibaseprog0100100200200300300400400370.9370.9269.8269.8285.4285.4370.2370.2Mean time / lemma (s) Figure 4: Per-module results on the Iris core (base = base_logic, prog = program_logic). Over the 4,1234,123 lemmas (96.9%96.9\%) with module-qualified log paths; the remaining 134134 have ambiguous file names (e.g. big_op.v occurs in two modules) and are omitted. VI-C Rust Standard Libraries To test whether Aria’s competence extends beyond the Iris core to the verified software built on it, we ran the same agent and hardened harness on RustBelt, the Iris-based verification of Rust that gives the first formal soundness proof for Rust’s ownership-based type system, including the unsafe code in its standard library [29]. We target Rust’s libraries for concurrency and interior mutability (Arc, Rc, Mutex, RwLock, RefCell, Cell, …), which build with a make-based toolchain rather than Iris’s dune setup, but are otherwise driven by the identical protocol: strip each lemma’s proof, let Aria derive a new one, and accept it only when the Coq kernel checks it. Aria proved 217 lemmas with zero failures across 25 files, 73% on the first attempt and 86% within a single retry; the hardest cases—such as the drop and clone proofs for Arc and the reader/writer guards of RwLock—took up to 13 retries. That Aria carries over—the same zero-failure outcome and first-try-dominated retry profile—from the Iris core to a downstream, real-world Rust-safety development is evidence the result is not an artifact of overfitting to a single corpus. TABLE IV: Aria on the Rust libraries verified in RustBelt. Library #Lemmas Library #Lemmas RwLock 36 Rc 30 RefCell 35 Mutex 20 Arc 33 Vec 17 Cell 35 Option 11 VI-D reglang reglang is a Coq library of regular-language theory—finite automata, regular expressions, and their equivalences. Unlike the Iris core and RustBelt, its proofs involve neither separation logic nor concurrency but instead underpin string-type verification in programming languages; we include it because, among the twelve projects in the CoqStoq benchmark [61]—which draws on the CoqGym [64] projects that compile under Coq 8.18, together with the CompCert verified C compiler and several actively maintained Coq-Community libraries—reglang is the one on which prior LLM provers such as Rango fare worst, proving barely one in eight, which makes it a direct comparison against prior work on its hardest case. We apply the identical protocol: strip each lemma’s proof and accept a new one only when the Coq kernel checks it. Aria proves all 318 lemmas with zero failures, 75.5% on the first attempt and a mean of 0.38 retries per lemma—the lowest retry rate of the three Coq benchmarks, consistent with reglang being the least demanding target. No proof required more than six retries. The averages hide one striking outlier, however: nfa_ofP—the correctness of a two-way finite-automaton construction—was the single longest-running proof in the entire study, taking roughly 5.8 hours and four retries to land (longer even than the hardest Iris lemma, at 4.7 hours). Where prior LLM provers clear barely one in eight of these proofs, Aria proves them all. VI-E Cross-Benchmark Comparison Figure 5 compares Aria across the three Coq developments on four per-lemma metrics: the first-attempt success rate, the mean and maximum number of retries, and the mean model time per lemma. The profile is consistent across all three: a first-attempt rate in the 7373–79%79\% range and a mean of well under one retry per lemma, with the Iris core—the largest and hardest target—posting both the highest first-attempt rate and the longest retry tail (up to 28). The RustBelt proofs are the most expensive on average (706706 s per lemma, roughly double the others), reflecting their greater length rather than a higher failure rate. IrisRustBeltreglang0202040406060808010010079.279.272.872.875.575.5First-attempt (%)IrisRustBeltreglang00.50.5110.510.510.850.850.380.38Mean retriesIrisRustBeltreglang01010202030302828131366Max retriesIrisRustBeltreglang0200200400400600600800800321.1321.1706706364.6364.6Mean time / lemma (s) Figure 5: Cross-benchmark comparison of Aria on the Iris core (4,257 lemmas), RustBelt (217), and reglang (318). VI-F iris-lean: Lemmas with No Prior Proof Our final benchmark pushes on two axes at once: a different proof assistant (Lean), and lemmas whose Lean proofs have never existed and so could not have been learned by the state-of-the-art model. Because Iris is so widely used, an effort is underway to port it to Lean 4—iris-lean [58]—but the port is far from finished, and a public tracker [59] shows which files have not yet been added. We pick three of these not-yet-ported files (Function, Mra, and UFrac), and task Aria with supplying the proofs. Soundness is now decided by the Lean kernel rather than Coq’s—the same harness design retargeted to a different verifier. Aria proves all 72 lemmas with zero failures, 90.3% on the first attempt and a mean of 0.10 retries—no proof needed more than one retry—in under two hours, the cleanest profile of any benchmark in this study. It also shows the harness + code agent approach is not tied to Coq: the same design works with the Lean kernel as the verifier. A direct comparison is instructive. On the three corresponding modules in upstream Coq Iris (functions.v, mra.v, ufrac.v; 49 lemmas), Aria proves every lemma but at a 75.5%75.5\% first-attempt rate, up to four retries, and 149149 s per lemma. The Lean port states the same algebra as more, smaller lemmas (7272 vs. 4949), and on these finer obligations Aria is markedly cleaner: 90.3%90.3\% first-attempt, never more than one retry, and 9797 s per lemma. The lesson is methodological—splitting a development into smaller lemmas gives the agent simpler obligations, raising the first-attempt rate and lowering per-lemma time. VI-G Private vs. Open-Source Models To compare the effectiveness and efficiency of a private and an open-source model, we re-ran a fixed benchmark—the 40 lemmas of iris/algebra/lib/frac_auth.v—under two models, holding the same Claude Code agent, harness, workflows, and prompts: the private Claude Opus 4.7 and the open-source Kimi K2.6, served through Ollama Cloud behind an Anthropic-compatible API. Figure 6 reports the outcome. On this subset both models proved all 40 lemmas, so an open-source model is clearly usable for the task; the visible difference is efficiency. The private model solved 72.5% of the lemmas on the first attempt, never needed more than three retries, and finished all 40 lemmas in under two hours; the open model solved 55% on the first attempt, occasionally needed many retries (up to 24), and took roughly seven times as long. We additionally ran DeepSeek V4 Pro, also through Ollama Cloud, under the identical setup (not shown in Figure 6); its results closely tracked Kimi’s—all 40 lemmas proved with a comparable retry profile—but at roughly two to three times the token consumption. The picture changes on harder proofs, however. These 40 lemmas have short proofs, which is precisely why the open model keeps up; across the wider library we observed a genuine capability gap on long proofs. Lemmas whose proofs run beyond roughly fifty lines frequently defeated the open model even after it exhausted the 30-retry budget; Opus 4.7, by contrast, proved them, reliably constructing and maintaining correct proofs of more than two hundred lines. 1st-attempt (%)mean retriesmax retriestime/lemma (s)72.50.40316955.01.77241253Opus 4.7Kimi K2.6 Figure 6: Private (Claude Opus 4.7) vs. open-source (Kimi K2.6). VI-H Rubric Criteria for Proof Polishing To illustrate the stylistic differences between human-written and LLM-generated proofs, we compare two correct proofs of the same proof obligation: discrete_cmra_mixin (a Definition that, like a lemma, is built by a proof and checked by the Coq kernel). Human proof. The expert-written proof is concise, relying on advanced tactic combinators and domain intuition to dispatch goals efficiently. ⬇ Definition discrete_cmra_mixin : CmraMixin A. Proof. destruct ra_mix; split; try done. - intros x; split; first done. by move=> /(_ 0i). - intros n x y1 y2 ??; by exists y1, y2. Qed. LLM proof (first stage). As first generated, the LLM proof is more verbose, addressing each subgoal explicitly rather than relying on compact tactic idioms. ⬇ Proof. destruct ra_mix. split. - intros x n. apply ra_op_proper0. - intros n x y cx. apply ra_core_proper0. - intros n. apply ra_validN_proper0. - intros x. split; [done|intros Hv; apply (Hv 0i)]. - intros n n’ x ? ?. done. - done. - done. - done. - done. - done. - done. - intros n x y1 y2 _ Hx. exists y1, y2. split_and!; done. Qed. Both proofs are accepted by Coq, yet they differ in style. The human proof uses try done to clear the routine subgoals at once, leaving a compact body; the first-stage LLM proof instead enumerates every subgoal, including a long run of bare done—correct, but verbose and brittle. Correctness, however, is the only hard constraint the Coq harness enforces; proof style is not. To improve style we add a second, soft harness: a set of rubric criteria that a good proof should satisfy: • Conciseness: collapse routine, repeated closers and drop no-op steps. • Transparency: keep each subgoal a legible step—no monolithic combinator blobs (e.g. a long first […]). • Robustness: avoid dependence on the number, order, or auto-generated names of subgoals. • Idiomatic style: follow the library’s conventions and tactic idioms. • Reuse: invoke existing lemmas rather than re-deriving them. Aria applies these in a second stage. A prover agent first produces a proof the Coq harness accepts; a separate polish agent—started fresh, sharing none of the prover’s context—is then handed that proof. The soft harness scores it against each criterion and returns feedback only for the ones it fails; the polish agent rewrites accordingly, and the Coq harness re-checks every rewrite so polishing can never break correctness. This repeats until all criteria pass or a cap of two polishing rounds is reached—if some criteria still fail after that, the already-correct proof is kept as is. Running this stage on the proof above yields: ⬇ Definition discrete_cmra_mixin : CmraMixin A. Proof. destruct ra_mix; split; try done. - intros x. split; [done|by intros Hv; apply (Hv 0i)]. - intros n x y1 y2 _ Hx. by exists y1, y2. Qed. The polished proof recovers the expert style: try done collapses the routine cases, and only the two substantive obligations remain as explicit bullets—matching the human proof in length and structure while staying fully machine-checked. VII Discussion The deeper lesson of this work is not about Iris in particular but about where the proof strategy should live. Reading the agents’ logs, the striking thing is how much of each proof is strategic decision-making that the model carries out entirely on its own. The agent decides what to do next. A code agent follows no fixed proof procedure; at every step it uses the LLM, and nothing else, to choose the proof’s direction—which prior lemma or hypothesis to apply, how to break a goal into subgoals and in what order, when to search the source for a definition it needs, which tactic to try, and when to abandon a line and backtrack. A recurring pattern across the logs is that the agent first looks for similar lemmas already in scope and mimics their proofs, adapting a nearby, structurally related argument rather than building each one from first principles. This is a strikingly human-like way to prove—the same instinct an expert relies on when reaching for an analogous lemma instead of starting over. These are exactly the decisions prior systems hard-wire. Where a trained premise selector, a proof-tree search, and a divide-and-conquer module each fix one choice in advance, our method delegates all three to the agent’s judgment—no premise model, no search policy, no decomposition heuristic. Because these decisions are made in context and per lemma rather than imposed uniformly by an external policy, a deliberately coarse loop of agent plus verifier clears proofs that defeated systems built around elaborate search. VIII Related Work We review prior automation along a single axis—how much of the proving it hands to a large language model—running from classic symbolic methods, through learned tactic search, to the model-in-the-loop agents closest to ours. Classic symbolic automation. Hammers discharge a goal by translating it to a first-order or SMT problem and reconstructing the result—CoqHammer [14] and Sledgehammer [7], with Thor [27] adding a language model for premise selection. They are effective on first-order goals—CoqHammer closes roughly 40% of the Coq standard library push-button—but a poor fit for the higher-order, step-indexed, separation-logic obligations that dominate Iris. Within Iris, the Iris Proof Mode and MoSeL [37, 35] and Diaframe [44] cut proof effort but are expert-engineered, and non-routine proofs still demand human guidance. Apart from Thor’s learned premise selection, these methods involve no machine learning. Tactic prediction and proof search. A decade of work learned to predict tactics from corpora of human proofs and combine them with search over the proof tree—ASTactic on CoqGym [64], Proverbot9001 [52], Tactician [6], Graph2Tac [5], the goal-adaptive Gpass [13], and the diversity-driven ensemble Diva [18]—the difficulty lying in premise selection and efficient search. A parallel line invests in search itself: HyperTree Proof Search [39] couples a neural prover with AlphaZero-style search, setting records on Metamath and Lean. These systems treat proving as guided search; their effort goes into the search policy rather than the verification contract around the model. LLM-based proof generation. LLMs shifted the emphasis toward generating whole proofs or large fragments, often with premise retrieval and feedback-driven repair: Baldur [19] and Draft-Sketch-Prove [28] for Isabelle, LeanDojo [65] and DeepSeek-Prover [63] for Lean, GPT-f [47] for Metamath, PALM [41], Rango [61], COPRA [56], and the divide-and-conquer Cobblestone [33] for Coq, and proof-oriented programming in F⋆ [12]. As Table I summarizes, these are fully automatic but partial—the strongest prove roughly 12–48% of their benchmarks—and evaluate on general-purpose, sequential developments such as CompCert. Closest to our setting, Cobblestone also checks every candidate with the Coq kernel, yet reaches 48% fully automatically (58% with oracle guidance) on general Coq. Aria differs on both axes: it targets the higher-order, concurrent separation logic of Iris and proves its four core modules completely. Verifier-in-the-loop agents and harnesses. Pairing a model with a checker and feeding back its errors is by now common—for proof repair [19] and in-context proof agents [56], and more broadly in autonomous agents for software tasks such as program repair [8]. Our contribution is twofold. First, we make the harness a first-class, declarative artifact: HHL lets the policy governing the agent be written, audited, and retargeted across agent runtimes. Second, we show that a sound verifier—the prover as an infallible oracle [18]—is necessary but not sufficient: when an agent can rewrite the proof file freely, it can satisfy the verifier while silently dropping or weakening the target lemma, leaving the file type-checking yet the task undone. The harness must therefore also enforce completeness—checking that the target lemma is still present, unweakened, and actually proved. This is easy to overlook once an agent edits files freely. IX Conclusion We presented Aria, which proves theorems fully automatically by pairing a general LLM code agent with a verification harness. Running unattended, it proved all 4,257 lemmas of the four core Iris modules, 217 RustBelt lemmas, and all 318 reglang lemmas—with zero Coq expert intervention and no failures, the first time an entire expert-grade concurrent separation-logic library has been proved automatically and in full. The recipe is deliberately coarse: the agent makes every proof-strategy decision while the harness, captured as reusable infrastructure in HHL, keeps it honest. A natural next step is to apply the same agent-plus-harness recipe upstream, to generating the formal specifications that proving presupposes. References [1] C. Allain and G. Scherer (2026) Zoo: a framework for the verification of concurrent ocaml 5 programs using separation logic. Proceedings of the ACM on Programming Languages 10 (POPL), p. 1702–1729. External Links: Document Cited by: §I. [2] Anthropic (2025)Claude code sdk(Website) Note: Programmatic runtime for building agents on the Claude Code agent harness (hooks, tool dispatch, and model access) External Links: Link Cited by: §I, §IV-B. [3] A. Azevedo de Amorim, A. Ahmed, and M. Gaboardi (2026) Cryptis: cryptographic reasoning in separation logic. Proceedings of the ACM on Programming Languages 10 (POPL), p. 2555–2585. External Links: Document Cited by: §I. [4] Y. Bertot and P. Castéran (2004) Interactive theorem proving and program development: coq’art–the calculus of inductive constructions. Springer Science+ Business Media. External Links: Document Cited by: §I. [5] L. Blaauwbroek, M. Olsák, J. Rute, F. I. Schaposnik Massolo, J. Piepenbrock, and V. Pestun (2024) Graph2Tac: online representation learning of formal math concepts. In Proceedings of the 41st International Conference on Machine Learning (ICML), Proceedings of Machine Learning Research, Vol. 235, p. 4046–4076. Cited by: TABLE I, §I, §I, §VIII. [6] L. Blaauwbroek, J. Urban, and H. Geuvers (2020) The tactician: a seamless, interactive tactic learner and prover for coq. In Intelligent Computer Mathematics (CICM), Lecture Notes in Computer Science, Vol. 12236, p. 271–277. External Links: Document Cited by: §I, §I, §VIII. [7] S. Böhme and T. Nipkow (2010) Sledgehammer: judgement day. In International Joint Conference on Automated Reasoning (IJCAR), p. 107–121. External Links: Document Cited by: §VIII. [8] I. Bouzenia, P. Devanbu, and M. Pradel (2025) RepairAgent: an autonomous, LLM-based agent for program repair. In Proceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), p. 2188–2200. External Links: Document Cited by: §VIII. [9] T. Chajed, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich (2019) Verifying concurrent, crash-safe systems with perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), p. 243–258. External Links: Document Cited by: §I. [10] T. Chajed, J. Tassarotti, M. Theng, R. Jung, M. F. Kaashoek, and N. Zeldovich (2021) GoJournal: a verified, concurrent, crash-safe journaling system. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), p. 423–439. Cited by: §I. [11] T. Chajed, J. Tassarotti, M. Theng, M. F. Kaashoek, and N. Zeldovich (2022) Verifying the daisynfs concurrent and crash-safe file system with sequential reasoning. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI), p. 447–463. Cited by: §I. [12] S. Chakraborty, G. Ebner, S. Bhat, S. Fakhoury, S. Fatima, S. K. Lahiri, and N. Swamy (2025) Towards neural synthesis for SMT-assisted proof-oriented programming. In Proceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), p. 1755–1767. External Links: Document Cited by: §VIII. [13] Y. Chen, Z. Sun, G. Wang, and D. Hao (2025) Gpass: a goal-adaptive neural theorem prover based on Coq for automated formal verification. In Proceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE), p. 653–665. External Links: Document Cited by: §VIII. [14] Ł. Czajka and C. Kaliszyk (2018) Hammer for coq: automation for dependent type theory. Journal of Automated Reasoning 61 (1–4), p. 423–453. External Links: Document Cited by: §VIII. [15] H. Dang, J. Jourdan, J. Kaiser, and D. Dreyer (2020) RustBelt meets relaxed memory. Proceedings of the ACM on Programming Languages 4 (POPL), p. 34:1–34:29. External Links: Document Cited by: §I. [16] P. E. de Vilhena and F. Pottier (2021) A separation logic for effect handlers. Proceedings of the ACM on Programming Languages 5 (POPL), p. 33:1–33:28. External Links: Document Cited by: §I. [17] C. Doczkal, J. Kaiser, and G. Smolka (2024)Regular language representations in coq(Website) External Links: Link Cited by: §VI-A. [18] E. First and Y. Brun (2022) Diversity-driven automated formal verification. In Proceedings of the 44th International Conference on Software Engineering (ICSE), p. 749–761. External Links: Document Cited by: §VIII, §VIII. [19] E. First, M. N. Rabe, T. Ringer, and Y. Brun (2023) Baldur: whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), p. 1229–1241. External Links: Document Cited by: §I, §VIII, §VIII. [20] D. Frumin, R. Krebbers, and L. Birkedal (2021) Compositional non-interference for fine-grained concurrent programs. In 2021 IEEE Symposium on Security and Privacy (SP), p. 1416–1433. External Links: Document Cited by: §I. [21] L. Gäher, M. Sammler, R. Jung, R. Krebbers, and D. Dreyer (2024) RefinedRust: a type system for high-assurance verification of rust programs. Proceedings of the ACM on Programming Languages 8 (PLDI), p. 1115–1139. External Links: Document Cited by: §I. [22] L. Gäher, M. Sammler, S. Spies, R. Jung, H. Dang, R. Krebbers, J. Kang, and D. Dreyer (2022) Simuliris: a separation logic framework for verifying concurrent program optimizations. Proceedings of the ACM on Programming Languages 6 (POPL), p. 28:1–28:31. External Links: Document Cited by: §I. [23] A. L. Georges, A. Guéneau, T. Van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal (2024) Cerise: program verification on a capability machine in the presence of untrusted code. Journal of the ACM 71 (1), p. 1–59. External Links: Document Cited by: §I. [24] A. Guéneau, J. Hostert, S. Spies, M. Sammler, L. Birkedal, and D. Dreyer (2023) Melocoton: a program logic for verified interoperability between ocaml and c. Proceedings of the ACM on Programming Languages 7 (OOPSLA2), p. 716–744. External Links: Document Cited by: §I. [25] J. K. Hinrichsen, J. Bengtson, and R. Krebbers (2020) Actris: session-type based reasoning in separation logic. Proceedings of the ACM on Programming Languages 4 (POPL), p. 6:1–6:30. External Links: Document Cited by: §I. [26] Z. Ji, N. Lee, R. Frieske, T. Yu, D. Su, Y. Xu, E. Ishii, Y. Bang, A. Madotto, and P. Fung (2023) Survey of hallucination in natural language generation. ACM Computing Surveys 55 (12), p. 1–38. External Links: Document Cited by: §I. [27] A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygóźdź, P. Miłoś, Y. Wu, and M. Jamnik (2022) Thor: wielding hammers to integrate language models and automated theorem provers. In Advances in Neural Information Processing Systems 35 (NeurIPS), Cited by: §VIII. [28] A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and C. Szegedy (2023) Draft, sketch, and prove: guiding formal theorem provers with informal proofs. In Proceedings of the 11th International Conference on Learning Representations (ICLR), Cited by: §I, §VIII. [29] R. Jung, J. Jourdan, R. Krebbers, and D. Dreyer (2018) RustBelt: securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages 2 (POPL), p. 66:1–66:34. External Links: Document Cited by: §I, §I, §VI-C. [30] R. Jung, R. Krebbers, L. Birkedal, and A. Bizjak (2015) Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 637–650. External Links: Document Cited by: §I, §I. [31] R. Jung, R. Krebbers, and L. Birkedal (2023)Iris: proof mode documentation and case studies(Website) External Links: Link Cited by: §I, §I. [32] R. Jung, R. Krebbers, J. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer (2018) Iris from the ground up: a modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28, p. e20. External Links: Document Cited by: §I, §I. [33] S. R. Kasibatla, A. Agrawal, Y. Brun, S. Lerner, T. Ringer, and E. First (2026) Cobblestone: a divide-and-conquer approach for automating formal verification. In Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE), p. 714–726. External Links: Document Cited by: TABLE I, §I, §VIII. [34] Z. Kaufman, E. First, A. Sanchez-Stern, K. Thompson, S. Lerner, and Y. Brun (2026) ProofCoop: collaborative automated formal verification. In Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE), p. 1339–1352. External Links: Document Cited by: TABLE I. [35] R. Krebbers, J. Jourdan, R. Jung, J. Tassarotti, J. Kaiser, A. Timany, A. Charguéraud, and D. Dreyer (2018) MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages 2 (ICFP), p. 77:1–77:30. External Links: Document Cited by: §VIII. [36] R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer, and L. Birkedal (2017) The essence of higher-order concurrent separation logic. In Programming Languages and Systems (ESOP), p. 696–723. External Links: Document Cited by: §I, §I. [37] R. Krebbers, A. Timany, and L. Birkedal (2017) Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), p. 205–217. External Links: Document Cited by: §VIII. [38] M. Krogh-Jespersen, A. Timany, M. E. Ohlenbusch, S. O. Gregersen, and L. Birkedal (2020) Aneris: a mechanised logic for modular reasoning about distributed systems. In Programming Languages and Systems (ESOP), Lecture Notes in Computer Science, Vol. 12075, p. 336–365. External Links: Document Cited by: §I. [39] G. Lample, T. Lacroix, M. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet (2022) HyperTree proof search for neural theorem proving. In Advances in Neural Information Processing Systems 35 (NeurIPS), Cited by: §VIII. [40] Z. Liu, S. Stepanenko, J. Pichon-Pharabod, A. Timany, A. Askarov, and L. Birkedal (2023) VMSL: a separation logic for mechanised robust safety of virtual machines communicating above f-a. Proceedings of the ACM on Programming Languages 7 (PLDI), p. 1438–1462. External Links: Document Cited by: §I. [41] M. Lu, B. Delaware, and T. Zhang (2024) Proof automation with large language models. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE), p. 1509–1520. External Links: Document Cited by: TABLE I, §I, §I, §I, §VIII. [42] Y. Matsushita, X. Denis, J. Jourdan, and D. Dreyer (2022) RustHornBelt: a semantic foundation for functional verification of rust programs with unsafe code. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), p. 841–856. External Links: Document Cited by: §I. [43] G. Mével, J. Jourdan, and F. Pottier (2020) Cosmo: a concurrent separation logic for multicore ocaml. Proceedings of the ACM on Programming Languages 4 (ICFP), p. 96:1–96:29. External Links: Document Cited by: §I. [44] I. Mulder, R. Krebbers, and H. Geuvers (2022) Diaframe: automated verification of fine-grained concurrent programs in iris. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), p. 809–824. External Links: Document Cited by: §VIII. [45] T. Nipkow, L. C. Paulson, and M. Wenzel (2002) Isabelle/hol: a proof assistant for higher-order logic. Lecture Notes in Computer Science, Vol. 2283, Springer. External Links: Document Cited by: §I. [46] P. W. O’Hearn, J. C. Reynolds, and H. Yang (2001) Local reasoning about programs that alter data structures. In Computer Science Logic (CSL 2001), Lecture Notes in Computer Science, Vol. 2142, p. 1–19. External Links: Document Cited by: §I, §I. [47] S. Polu and I. Sutskever (2020) Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393. External Links: Document Cited by: §I, §VIII. [48] X. Rao, A. L. Georges, M. Legoupil, C. Watt, J. Pichon-Pharabod, P. Gardner, and L. Birkedal (2023) Iris-wasm: robust and modular verification of webassembly programs. Proceedings of the ACM on Programming Languages 7 (PLDI), p. 1096–1120. External Links: Document Cited by: §I. [49] M. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon-Pharabod, D. Dreyer, D. Garg, and P. Sewell (2022) Islaris: verification of machine code against authoritative isa semantics. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), p. 825–840. External Links: Document Cited by: §I. [50] M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg (2021) RefinedC: automating the foundational verification of c code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), p. 158–174. External Links: Document Cited by: §I. [51] M. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, and D. Dreyer (2023) DimSum: a decentralized approach to multi-language semantics and verification. Proceedings of the ACM on Programming Languages 7 (POPL), p. 775–805. External Links: Document Cited by: §I. [52] A. Sanchez-Stern, Y. Alhessi, L. Saul, and S. Lerner (2020) Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL), p. 1–10. External Links: Document Cited by: TABLE I, §I, §I, §VIII. [53] U. Sharma, R. Jung, J. Tassarotti, M. F. Kaashoek, and N. Zeldovich (2023) Grove: a separation-logic library for verifying distributed systems. In Proceedings of the 29th ACM Symposium on Operating Systems Principles (SOSP), p. 113–129. External Links: Document Cited by: §I. [54] S. Spies, L. Gäher, M. Sammler, and D. Dreyer (2024) Quiver: guided abductive inference of separation logic specifications in coq. Proceedings of the ACM on Programming Languages 8 (PLDI), p. 889–913. External Links: Document Cited by: §I. [55] C. D. Team (2004) The coq proof assistant. Available at: https://coq.inria.fr. Cited by: §I. [56] A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri (2024) An in-context learning agent for formal theorem-proving. In Proceedings of the 1st Conference on Language Modeling (COLM), Cited by: TABLE I, §I, §I, §I, §VIII, §VIII. [57] The Iris Team (2024)The iris coq development(Website) External Links: Link Cited by: §VI-A. [58] The Iris-Lean Developers (2025)Iris-lean: a port of the iris separation logic framework to lean 4(Website) External Links: Link Cited by: §VI-A, §VI-F. [59] The Iris-Lean Developers (2025)Iris-lean: porting progress tracker(Website) External Links: Link Cited by: §VI-F. [60] The RustBelt Team (2024)The lambda-rust (rustbelt) coq development(Website) External Links: Link Cited by: §VI-A. [61] K. Thompson, N. Saavedra, P. Carrott, K. Fisher, A. Sanchez-Stern, Y. Brun, J. F. Ferreira, S. Lerner, and E. First (2025) Rango: adaptive retrieval-augmented proving for automated software verification. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE), p. 347–359. External Links: Document Cited by: TABLE I, §I, §I, §I, §I, §VI-A, §VI-D, §VIII. [62] A. Timany, S. O. Gregersen, L. Stefanesco, J. K. Hinrichsen, L. Gondelman, A. Nieto, and L. Birkedal (2024) Trillium: higher-order concurrent and distributed separation logic for intensional refinement. Proceedings of the ACM on Programming Languages 8 (POPL), p. 241–272. External Links: Document Cited by: §I. [63] H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang (2024) DeepSeek-prover: advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333. External Links: Document Cited by: §I, §VIII. [64] K. Yang and J. Deng (2019) Learning to prove theorems via interacting with proof assistants. In Proceedings of the 36th International Conference on Machine Learning (ICML), Proceedings of Machine Learning Research, Vol. 97, p. 6984–6994. Cited by: TABLE I, §I, §I, §VI-D, §VIII. [65] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar (2023) LeanDojo: theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems 36 (NeurIPS), Datasets and Benchmarks Track, Cited by: §I, §VIII.

Instant research discovery