Schwarz: Solver-Aware Agentic Program Verification
2026-08-31 • Logic in Computer Science
Logic in Computer ScienceSoftware Engineering
AI summaryⓘ
The authors present Schwarz, a tool that helps computer programs prove that code is correct by fixing small parts of failed proofs instead of giving up completely. When usual tools fail to verify code, they only show a general error, but Schwarz breaks down the problem into smaller, manageable pieces that can be checked and fixed locally. It uses smart strategies to handle different math problems the solver faces and was tested on many tasks in C and Rust code, solving over 90% successfully. Their results show that breaking down proof failures and guiding repairs based on the solver’s needs work better than previous methods.
Agentic verificationSMT solverProof obligationsLocal repairVerification harnessHelper lemmasTheory-aware policiesC/Rust verificationSV-COMPCPAchecker
Authors
Jingyu Ke, Ling-I Wu, Guoqiang Li
Abstract
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.