Source-linked AI summary
Schwarz: Solver-Aware Agentic Program Verification
Jingyu Ke, Ling-I Wu, Guoqiang Li
TL;DR
Agentic verification needs more than plausible source-level specifications: failed SMT proofs must reveal local, checkable repair targets. Schwarz provides snapshots, local lemmas, and theory-aware solver policies, solving 95.2% of recent agentic-verification benchmarks and 91.5% of SV-COMP tasks versus 60.1% for CPAchecker.
Problem
Plausible source-level specifications often fail to become SMT obligations that solvers can prove, while current loops expose only coarse errors and obscure the local cause of failure.
Method
Schwarz converts failed verification into obligation-local repair using checked program-point snapshots, SMT-local lemmas, and theory-aware solver policies.
Results
Schwarz solves 95.2% of 475 existing agentic-verification tasks and 91.5% of 1,000 SV-COMP 2026 ReachSafety tasks, compared with 60.1% for CPAchecker.
Takeaways & Limitations
Across 1,475 tasks, solver-aware repair supports checked, solver-facing verification while remaining tied to source-level annotations and local obligations.
Takeaways & Limitations
Results may be affected by model nondeterminism, incomplete prototype coverage, and semantic regions that Schwarz does not yet fully support.
Abstract
from arXiv · showhide
Agentic verification systems can often generate source-level specifications that look plausible, but plausibility is not enough: the verifier must still turn those specifications into SMT obligations that the solver can prove. When this step fails, current LLM-driven loops usually expose only a coarse verifier error, timeout, or unknown solver result. The model cannot tell whether the specification is wrong, a helper lemma is missing, the proof context contains irrelevant facts, or the obligation needs a different theory view. This paper presents Schwarz, an agentic verification harness that makes SMT-backed proof failure local, checkable, and repairable. Schwarz turns failed verification into obligation-local repair tasks: program-point snapshots expose checked facts at a boundary, local lemmas let the agent propose missing proof steps, and theory-aware solver policies guide the agent toward solver-friendly formulations for numeric, quantified, memory, and floating-point obligations. We implement Schwarz for C and Rust/Verus and evaluate it on 1,475 tasks. On 475 benchmarks from recent agentic verification tools, Schwarz solves 95.2% of the tasks. On 1,000 tasks from the SV-COMP 2026 ReachSafety track, averaging 1,427 LOC, Schwarz solves 91.5% of the tasks, compared with 60.1% for CPAchecker. Ablations and comparison with a pure-agent baseline show that solver-aware repair is effective and scalable.
I. INTRODUCTION
SMT-backed agentic verification fails when plausible specifications do not yield solver-dischargeable obligations, while existing loops expose too little diagnostic context. Schwarz addresses this with obligation-local repair, theory-aware guidance, and deterministic checking, achieving high solve rates across two benchmark settings.
- Approach: A local bridge for C integer-promotion semantics lets the verifier prove the final target by separately checking arithmetic agreement and definedness.This avoids requiring a top-level bit-vector query to rediscover the promotion reasoning.
- Trust model: The model searches over specifications, decompositions, lemmas, policies, and counterexamples, while trusted checking, SMT solving, and concrete replay determine accepted outcomes.The harness does not accept model rationale as a correctness certificate.
- Evaluation: Schwarz evaluates 1,475 tasks, solving 95.2% of 475 recent agentic-verification benchmarks and 91.5% of 1,000 SV-COMP 2026 ReachSafety tasks.The SV-COMP suite averages 1,427 LOC.
- Motivation: SMT-backed agentic verification is bottlenecked by solver dischargeability: plausible specifications can fail because local lemmas, relevant context, or suitable theory formulations are missing.Current failures may appear only as failed assertions, timeouts, or unknown solver results.
- Approach: Schwarz turns failed verifier runs into checked, obligation-local repair tasks using program-point snapshots, local lemmas, and theory-aware solver policies.The policies target numeric, quantified, memory, and floating-point obligations.
II. BACKGROUND
Deductive verification reduces specified programs to logical obligations that must be discharged before acceptance. SMT solvers handle these obligations across multiple theories, but success depends on encoding, context, and solver heuristics; Schwarz presents a trust-boundary workflow around this process.
- A. Deductive Verification: Deductive verification uses specifications such as contracts, assertions, loop invariants, frame conditions, and ghost state to instantiate program predicates and generate checked obligations.Obligations cover assertion, invariant, postcondition, call-contract, and frame-condition uses.
- B. SMT-backed Proof Discharge: SMT-backed verifiers encode obligations over arithmetic, arrays, bit-vectors, uninterpreted functions, and heap models, usually proving a target by checking whether its negation is unsatisfiable.Unsat accepts the proof step; sat, unknown, timeout, or translation failure rejects it.
- C. Agent Harnesses: Figure 2 places an untrusted agent above a trusted boundary and keeps hidden metadata and acceptance logic inside the harness.The agent sees anonymized source, target specifications, and compilation environments rather than verifier-side metadata.
- B. SMT-backed Proof Discharge: SMT success depends on theory, encoding, and query context, with quantified instantiation and arithmetic procedures introducing heuristic and computational limitations.Trigger choices can create matching loops or unstable verification times.
C. Agent Harnesses
Schwarz organizes verification as a layered agent harness in which the model explores repairs while deterministic infrastructure controls evidence and acceptance. Local feedback and explicit theory guidance reduce irrelevant solver context and repeated agent exploration.
- C. Agent Harnesses: An agent execution harness comprises execution, tools, context management, orchestration, observability, verification, and governance layers.Schwarz instantiates these with isolated workspaces, compilers, verifiers, snapshots, repair loops, logs, deterministic checking, and access rules.
- C. Agent Harnesses: Schwarz exposes anonymized source and target information to the agent while retaining comments, ground-truth labels, and acceptance logic below the trust boundary.This separates agent exploration from verifier authority.
- C. Agent Harnesses: The repair loop plans, generates or refines specifications, proposes counterexamples, invokes lemma repair, and uses theory-aware policies to select arithmetic, bit-vector, memory, or quantifier views.The checker retains the soundness decision.
- C. Agent Harnesses: For safe proofs, the checker regenerates obligations and requires SMT discharge; for unsafe answers, it accepts only witnesses validated by concrete replay.Unknown, timeout, or rejected artifacts do not become accepted outcomes.
- C. Agent Harnesses: Schwarz minimizes redundant solver context and redundant LLM exploration by making feedback local and recurring theory choices explicit.Snapshots limit accumulated irrelevant state, while solver-facing guidance discourages repeated solver-hostile formulations.
A. SMT-Local Lemmas
Schwarz localizes failed SMT proofs into inspectable obligations and checked decompositions, allowing agents to diagnose context, theory, or missing-lemma problems without rewriting the entire proof.
- A. SMT-Local Lemmas: The checker exposes each local obligation with its symbolic context, target fact, active theory view, and proof policy.The obligation is discharged by checking unsatτl(Γl ∧¬φl).
- A. SMT-Local Lemmas: When a query fails or times out, Schwarz reports the obligation and generated SMT file so the agent can inspect the solver-level failure.The agent can test whether missing semantics, irrelevant context, or a mismatched theory view explains the failure.
- A. SMT-Local Lemmas: An SMT-local lemma decomposes a failed local obligation into smaller facts that the checker independently justifies.The strengthened context must prove the target, and each proposed lemma must follow from already checked context.
- A. SMT-Local Lemmas: Direct SMT edits are diagnostic experiments, while accepted repairs must return to source-level annotations that the checker regenerates and validates.This preserves the distinction between hypothesis testing and trusted proof evidence.
- A. SMT-Local Lemmas: Short default solver timeouts provide faster diagnostic feedback about context size, theory choice, and missing lemmas.Compact obligations matching the intended theory are often discharged in milliseconds.
B. Theory-Aware Policies
Schwarz exposes theory selection and recurring proof decompositions as checked solver-facing policies, steering agents toward formulations that preserve source semantics while producing smaller, more tractable obligations.
- B. Theory-Aware Policies: Aggregate proofs are decomposed into scoped ghost-state updates and local inductive obligations instead of one global quantified formula.For prefix sums, the policy maintains a ghost prefix array through local updates such as Pi+1 = store(Pi, i + 1, select(Pi, i) + A[i]).
- B. Theory-Aware Policies: Global quantified aggregate formulas mix theories and program facts, making them poor solver targets and difficult for agents to repair locally.The policy addresses this by connecting smaller ghost-state obligations across loop steps.
- B. Theory-Aware Policies: Theory-aware policies let the agent choose obligation-specific formulations while the checker preserves the source program’s semantics.The interface supports selecting mathematical arithmetic or BitVec views rather than inheriting one global encoding.
- B. Theory-Aware Policies: BitVec often performs poorly on complex scalar arithmetic, whereas LIA/NIA or C-aware variants are recommended for value-level reasoning.BitVec remains appropriate when truth depends on truncation, wraparound, or raw bit layout.
- B. Theory-Aware Policies: The policy library captures recurring solver-theory priors as checked proof-artifact choices, reducing redundant exploration of semantically equivalent formulations.These choices guide representations for arrays, scalar induction summaries, and other theory-sensitive obligations.
C. Snapshot Mechanism
Snapshots make repair incremental by recording checked proof state at named program boundaries, allowing later steps to resume from compact local context rather than replaying the full exploration history.
- C. Snapshot Mechanism: A snapshot records a program point, checked in-scope facts, the active proof policy, and validated ghost or summary state.Later proof steps can resume from this boundary without reintroducing irrelevant facts.
- C. Snapshot Mechanism: Snapshots prevent long-program repair from being dominated by repeated revalidation of already checked prefixes.They retain only the compact state needed for the next transition.
- C. Snapshot Mechanism: Snapshots are caches for incremental engineering, not acceptance evidence; the final clean-gate check regenerates and verifies every obligation from the original source.The final pass ignores cached snapshot state.
V. IMPLEMENTATION
Schwarz combines language-specific trusted front ends, a shared SMT verification core, and a deterministic harness to run agentic repair across C and Rust/Verus verification tasks.
- V. IMPLEMENTATION: Schwarz is implemented for C and Rust in about 220K lines of non-test Rust code.Its architecture comprises trusted language front ends, a shared verification core, and a harness layer.
- V. IMPLEMENTATION: The shared core discharges front-end-generated obligations using CVC5, Bitwuzla, and Z3, classifying results as proved, refuted, unknown, or timed out.Short-timeout checks dispatch obligations to configured solvers in parallel.
- V. IMPLEMENTATION: The C front end translates annotations and semantic requirements into program-point obligations, including memory-safety conditions and unreachable-error-path checks.Queries typically encode premises with the negated target and ask for unsatisfiability.
- V. IMPLEMENTATION: C loop invariants and function contracts over-approximate behavior, supporting sound unreachable-state conclusions for executions represented by the trusted semantics.The Rust front end follows the same overall lowering pattern.
- V. IMPLEMENTATION: A deterministic protocol schedules the agent, invokes the backend checker, returns trusted diagnostics, and resumes repair iterations.The agent cannot inspect trusted front-end, checker, or orchestration internals.
A. Evaluation Setting
The evaluation spans 1,475 tasks across C and Rust/Verus settings, comparing Schwarz with agentic and traditional verification tools under a common evaluation framework. Results are reported per suite, with benchmark granularity and proof-artifact differences treated as evaluation constraints.
- Benchmark suites: The benchmark settings span C and Rust/Verus, including ReachSafety, NoOverflow, and single-file proof tasks.The C suites use source programs and the Rust/Verus portion uses 313 single-file proof tasks.
- Benchmark suites: The curated C suite is stratified by feature category and LOC bucket, covering loops, arrays, pointers, floating point, numeric reasoning, bit-level operations, and recursion.The suite excludes cases containing cyclic goto.
- Protocol: All tools run with a 4-hour wall-clock timeout per task, with agentic tools allowed unlimited model calls and repair rounds within that limit.Each task is limited to at most 8 CPU cores and 12 GB of memory.
- Compared systems: Schwarz is compared with AutoRocq, AutoVerus, KVerus, and CPAchecker across their respective benchmark and proof-artifact settings.The comparison maps each tool to its native verification interface rather than treating all artifacts as interchangeable.
- Headline results: Schwarz directly passes 1,367 of 1,475 tasks (92.7%), including 452 of 475 agentic-verification benchmarks (95.2%) and 915 of 1,000 SV-COMP tasks (91.5%).On the SV-COMP suite, CPAchecker passes 601 tasks (60.1%).
C. RQ2: Solver-Facing Interface
The ablation shows that solver-facing repair substantially improves verification, with SMT-local lemmas contributing more than theory-aware policies and both mechanisms complementing each other.
- RQ2: Solver-Facing Interface: 92.7% aggregate pass rate is achieved with the full solver-facing interface, compared with 73.3% when both components are disabled.The full configuration passes 1367/1475 tasks, while the combined ablation passes 1081.
- RQ2: Solver-Facing Interface: 77.7% aggregate pass rate remains without SMT-local lemmas, versus 92.7% with them, making lemmas the larger contributor.Disabling SMT-local lemmas loses 221 tasks, compared with 66 lost when theory-aware policies are removed.
- RQ2: Solver-Facing Interface: 88.2% aggregate pass rate without theory-aware policies shows a smaller but consistent benefit from solver-friendly theory choices.Policies lose 44 passes on VariousSVC-ReachSafety and 18 on KVerus-File when removed.
- RQ2: Solver-Facing Interface: Figure 4 organizes accepted passes by dominant source feature and LOC bucket, with each cell reporting accepted passes and pass rate.The figure covers the 1,000-task SV-COMP 2026 ReachSafety suite.
- RQ2: Solver-Facing Interface: The combined ablation is worse than either single ablation on three of four suites and in aggregate, indicating complementary mechanisms.Local lemmas decompose hard obligations, while policies help choose theory-sensitive decompositions that solvers can handle efficiently.
D. RQ3: Capability Boundaries
SCHWARZ performs strongly across several source features and program sizes, while its current capability boundary is concentrated in floating-point and semantic-coverage challenges.
- RQ3: Capability Boundaries: 915 accepted passes are distributed across feature and size buckets, including 119/120 recursion cases and 138/140 numeric cases below 100 LOC.It also solves 77/83 array-pointer cases and all 26 control-flow cases in the 100–1000 LOC bucket.
- RQ3: Capability Boundaries: 67/68 numeric cases in the 1000–5000 LOC bucket and 50/51 control-flow-heavy cases above 5000 LOC show capability beyond short programs.The pass-only metric remains high across multiple task types and LOC buckets.
- RQ3: Capability Boundaries: Floating-point tasks are least stable, with 89/114 passes below 100 LOC, 80/100 at 100–1000 LOC, and 12/22 above 5000 LOC.All 22 floating-point tasks in the 1000–5000 LOC bucket are solved.
- RQ3: Capability Boundaries: Many floating-point misses involve missing models for library and libm behavior, while other boundaries include long proof routes and layout-sensitive C constructs.Examples include sqrtf and tanf, aggressive snapshot placement needs, and unions or bit-level reinterpretation.
E. Threats to Validity
The paper positions SCHWARZ against agentic verification and SMT systems while qualifying its evaluation because benchmark units, nondeterminism, and semantic coverage differ across settings.
- Threats to Validity: The evaluation reports per-suite results because Rocq verification conditions, Verus proof artifacts, and C source programs are not interchangeable units.This avoids treating the aggregate as a universal leaderboard.
- Threats to Validity: Nondeterministic model outputs and incomplete prototype coverage may affect overall results, with unsupported semantic regions producing blocked runs.Multiple proof routes and theory choices can exist for the same specification.
- Related Work: Unlike Verus-level lemmas in AutoVerus and KVerus, SCHWARZ directly addresses solver-level unknown and timeout failures after lowering.This solver-level focus is identified as the core problem addressed by SCHWARZ.
- Related Work: Existing LLM-assisted SMT systems target particular theory fragments, whereas SCHWARZ combines local lemmas, snapshots, and theory policies in a program-verification harness.The comparison distinguishes SCHWARZ by scope and information source.
VIII. DISCUSSION
The discussion frames SCHWARZ as a harness-design approach: agents search over proof artifacts while deterministic infrastructure retains correctness authority and operationalizes domain expertise.
- VIII. DISCUSSION: SCHWARZ makes the path from source annotations to SMT queries explicit while keeping trusted lowering and checking outside agent control.This exposes information and control surfaces inside the agentic loop without delegating correctness judgments.
- VIII. DISCUSSION: Theory-aware policies encode expert knowledge directly, making solver-specific verification expertise operational within the repair loop.The discussion contrasts this with relying on base-model pretraining or accumulated long-term context.
- VIII. DISCUSSION: Across 1,475 tasks, SCHWARZ solves 1367 cases, including 95.2% of recent agentic-verification benchmarks and 91.5% of SV-COMP ReachSafety tasks.The remaining failures are described as mostly semantic coverage gaps.
- VIII. DISCUSSION: The authors manually checked figure content generated with generative AI for Figures 1 and 2.The disclosure concerns figure production rather than verification results.