Schwarz: Solver-Aware Agentic Program Verification

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and claims

Schwarz is a checked repair harness for SMT-backed C and Rust/Verus verification. Its premise is that a plausible source annotation can fail because a local lemma is missing, irrelevant facts pollute the context, or the encoding uses the wrong SMT theory. The paper defines “solver dischargeability” as requiring a fact to be true and expressed with enough local facts, decomposition, and theory encoding for the configured solver to prove it. The LLM proposes specifications, lemmas, decompositions, policies, and counterexamples; trusted front ends regenerate obligations and deterministic checkers accept only solver proofs or concrete replay. This separation is essential: “The model owns search: it proposes source-level specifications, proof decompositions, local lemmas, theory-aware solver policies, and counterexample inputs. The checker owns authority”.

technique 1: SMT-local lemmas

what it is and when to use it. Replace a global failed verification attempt with a small obligation at program point l: O_l = <l, Γ_l, φ_l, τ_l>, where Γ_l is the symbolic context, φ_l the target fact, and τ_l the active theory policy. Ask the solver to prove Γ_l |=τ_l φ_l, encoded as unsatisfiability of Γ_l ∧ ¬φ_l. Use this when a verifier reports timeout or unknown and a whole-program rewrite would obscure the actual missing step.

how to apply. Expose the failed obligation and generated SMT file. Let the agent hypothesize a bridge or intermediate lemma. First check that the lemmas together suffice, Γ_l ∧ m_1 ∧ … ∧ m_k |=τ_l φ_l, then check each proposed lemma sequentially: Γ_l ∧ m_1 … ∧ m_{i-1} |=τ_l m_i. Direct SMT edits are diagnostic only. Once a lemma works, translate it back into a source assertion, ghost fact, or contract; rerun the trusted front end from original source. The paper’s C example introduces a bridge for integer promotion and definedness so a final bit-vector assertion does not rediscover C arithmetic semantics. Local lemmas are checked decomposition, never unchecked assumptions.

verus form (inference). Write a Rust assert or ghost lemma at the failing program point, prove it from the current requires and invariant context, and then use it to discharge the next assertion. Keep the final proof in Verus source; an SMT file edited by an agent is an experiment, not evidence. ensures and requires provide the stable boundary, while assert forall|...| or a named proof fn lemma can encode reusable intermediate facts.

evidence and limits. Removing local lemmas reduces aggregate passes from 1367/1475 (92.7%) to 1146/1475 (77.7%); on 1,000 C ReachSafety tasks it falls from 915/1000 to 756/1000. The drop is largest on the 1,000-task C suite (91.5% to 75.6%), then KVerus-File (95.5% to 81.8%) and AutoRocq-ReachSafety (94.6% to 81.3%). Inference: since the paper’s residual failures are mostly missing semantic models, lemmas do not compensate for unsupported source semantics or missing library models.

technique 2: theory-aware solver policies

what it is. Policies tell the agent which checked formulation fits the obligation: use ghost prefix summaries for array aggregates; select mathematical integer arithmetic for value-level induction; reserve bit-vectors for truncation, wraparound, and layout. The paper warns that “Encoding every scalar obligation as BitVec preserves C integer semantics, but BitVec performs poorly on complex arithmetic”. Conversely, globally replacing machine integers with mathematical integers can be unsound.

how to apply. Classify the target by dominant theory. For a loop sum, introduce ghost prefix state P and local update P_{i+1}=store(P_i,i+1,select(P_i,i)+A[i]), then prove inductive invariants instead of one quantified aggregate. For scalar arithmetic, use LIA/NIA or C-aware variants; for raw machine behavior, use BitVec. The deterministic checker verifies that the selected theory preserves source semantics and that any bridge obligations are discharged.

verus form (inference). Choose Rust integer types and mathematical int specifications deliberately. Use ghost sequences/maps for prefix summaries, with loop invariants connecting executable updates to ghost state. Keep bit-precise facts in uN/iN specifications where overflow matters; add explicit cast and range lemmas rather than assuming mathematical arithmetic.

evidence and limits. Disabling policies lowers the aggregate to 1301/1475 (88.2%), a 66-task loss; disabling both policies and local lemmas gives 1081/1475 (73.3%). Policies are guidance, not proof, and their benefit is smaller on short arithmetic tasks already near solver saturation.

technique 3: checked snapshots and rapid failure

Snapshots are named proof boundaries containing a program point, checked in-scope facts, active policy, and validated ghost or summary state. The paper’s exact definition is: “A snapshot is a named boundary in the proof state”. Repair resumes from the snapshot without replaying irrelevant earlier exploration. At the end Schwarz ignores caches and runs a clean gate from original source, regenerating all obligations. It also normally uses aggressive local timeouts, often in the 10–20 second range, so unknown or timeout quickly distinguishes context, theory, and missing-lemma hypotheses; an agent may selectively extend a timeout for an intrinsically hard obligation.

verus form (inference). A snapshot corresponds to a proved intermediate lemma or function boundary whose postcondition summarizes prior execution. Reuse the lemma in later proof attempts, but run a clean cargo verus build from source before accepting the result. Timeouts remain diagnostic, never a soundness result.

evaluation, trust, and VL implications

Across 1,475 tasks, Schwarz directly passes 1367 (92.7%): 452/475 (95.2%) existing agentic-verification tasks and 915/1000 (91.5%) SV-COMP ReachSafety tasks. CPAchecker passes 601/1000 (60.1%). The pure-agent baseline scores 1212/1672 under SV-COMP penalties; Schwarz scores 1516/1672. The dominant residual failures are semantic coverage gaps—unsupported libm, string, union, and large-context cases—rather than simple timeout (13/1000 primarily time out). The evaluation mixes C, Rocq, and Rust/Verus suites, so aggregate comparisons are not interchangeable.

Inference from the paper’s description of the harness (it gives no single list): trusted components are source front ends, lowering, SMT solvers, concrete replay, hidden acceptance logic, and clean end-to-end regeneration. The model, direct SMT edits, and policy suggestions are untrusted. Inference for VL: the strongest reusable design is obligation-local feedback: expose the exact Verus VC, add checked bridge lemmas, and retain a clean proof gate. Inference, not the paper’s: the threat to agent-written verified Rust is that a solver-friendly lemma can still encode the wrong functional contract; solver dischargeability is necessary for proof progress, not evidence that the intended behavior was specified.

techniques for the catalog

• SMT-local lemma repair: decompose a timeout or unknown into a checked, program-point obligation and lift successful lemmas back into source
• theory-aware policy: choose ghost summaries, arithmetic, bit-vector, memory, or quantified encodings according to the obligation’s semantics
• proof snapshots: cache validated boundaries for local repair, then regenerate and check the entire proof from original source
• short diagnostic timeouts: fail local hypotheses quickly so the agent can test context and theory alternatives
• trust-boundary harness: keep lowering, solving, and concrete replay deterministic while the LLM searches untrusted artifacts

Audited 2026-10-12 against the paper: checked every count and percentage (Tables I, III, IV, Fig. 3, Section VI-B to VI-D), the obligation and lemma-check formulas, the prefix-sum update, the timeout range, the snapshot definition and clean gate, and all three quotations. Changed: two quotations now end before the paper’s punctuation (colon, comma) so they are verbatim; a claim that lemmas are strongest on KVerus replaced by the paper’s per-suite drops (largest on the C suite) with the generalisation marked as inference; the lemma-check order now includes the paper’s first sufficiency check; the 10-20 second timeouts now say often; Verus lemma naming corrected to proof fn; three unmarked study implications (trusted-component list, threat to verified Rust, VL design) marked as inference. Could not check: the Verus forms are the study’s own mapping and the paper has Verus only as a KVerus-File benchmark, so they were checked for Verus soundness only.

Last edited: 2026-10-13