跳转到内容
- Bottleneck = solver dischargeability: plausible source-level specs still fail because the harness only returns coarse error/timeout/unknown — agent can’t tell wrong-spec vs missing lemma vs irrelevant context vs wrong theory view.
- Schwarz turns failed verification into obligation-local repair: (1) program-point snapshots expose checked facts at a boundary; (2) SMT-local lemmas — agent proposes intermediate facts that must themselves be proved before use; may edit local SMT file diagnostically then lift success back to source annotations; (3) theory-aware solver policies (numeric / quantified / memory / FP / BitVec vs LIA-NIA) guide solver-friendly formulations.
- Trust boundary: model owns search; checker owns authority (regenerate VCs from trusted front ends, SMT unsat, or concrete replay for unsafe). Anonymized program view; hidden ground-truth metadata.
- Impl: ~220 KLOC Rust; C + Rust/Verus front ends; solvers cvc5, Bitwuzla, Z3 in parallel; short default timeouts 10–20s for fast hypothesis testing; final clean-gate regenerates all obligations end-to-end (snapshots ignored).
- 1,475 tasks aggregate → 1,367 / 92.7% accepted.
- 475 agentic-tool benches (AutoRocq ReachSafety/NoOverflow + KVerus-File) → 95.2% (452/475).
- 1,000 SV-COMP 2026 ReachSafety (avg 1,427 LOC) → 91.5% (915) vs CPAchecker 60.1% (601); pure-agent baseline SV-COMP score 72.5% → 90.7% with Schwarz (1516/1672 scoring units).
- Per-suite (Table III): AutoRocq-RS 106/112 (94.6%); AutoRocq-NoOverflow 47/50 (94.0%); KVerus-File 299/313 (95.5%) vs AutoVerus 217 (69.3%) / KVerus paper Claude 251 (80.2%).
- Ablation (Table IV): full 92.7% → no theory policies 88.2% (−66) → no SMT-local lemmas 77.7% (−221) → both off 73.3% (−286). Lemmas dominate.
- Failures: ~80% missing frontend/lib semantics (libm tanf/sqrtf, strncmp, unions); only 13/1000 primarily time-exhausted. Strong on numeric/recursion/large CF; weakest on FP + layout-sensitive C.
- Claim: no incorrect Schwarz-accepted verdicts.
- Expose local SMT obligation
O_l = ⟨l, Γ_l, φ_l, τ_l⟩ not just “Verus/Frama failed”.
- Short timeouts + parallel solvers as diagnostic signal; agent may extend selectively.
- Policy library encodes recurring priors (ghost prefix arrays for aggregates; LIA/NIA for value arithmetic, BitVec only for wrap/truncation).
- Snapshots for long routes; clean-gate prevents cache-trust.
- Adopt for Herdr: obligation-local repair + theory policies when using Verus/Dafny/SMT gates; trust boundary + anonymized task view. Compare: AutoVerus lemmas stay at Verus frontend — Schwarz goes below to SMT unknowns (complement, not replacement).
- Caveat: Rocq/ITP path has different cost profile (verbose context, replay bottleneck) — Schwarz is SMT-backed complementary design.
- Benchmark units not interchangeable (Rocq VCs vs Verus proofs vs C programs) — don’t treat 92.7% as universal. Prototype semantic gaps dominate misses. Confidence high on design thesis + ablations; medium on DIY portability until OSS harness available (paper doesn’t ship a public repo link in abstract).