arxiv-2605.21434-bmc-agent

Extract — BMC-Agent / Agentic Model Checking

URL: https://arxiv.org/abs/2605.21434 (read via https://arxiv.org/html/2605.21434)
Fetched: 2026-09-27 ~19:33 CST · defuddle parse —md
Authors: Youcheng Sun, Jiawen Liu, Daniel Kroening, Jason Xue (MBZUAI / Amazon)
Code: https://github.com/agentic-prover/aprover

Agentic model checking: LLM agents + BMC backend under agents propose, solvers verify. Agents do semantic judgment (spec inference, arithmetic-flag selection, CEx classification, refinement); BMC (CBMC for C, Kani for Rust) owns every soundness-relevant decision.
Three architectural commitments: (1) top-down per-function pre/post in a restricted DSL → deterministic translate to __CPROVER_assume/assert or kani::assume/assert, plus optional functional_spec for behavioural faithfulness beyond panic-freeness; (2) compositional assume-guarantee — each fn checked alone with callees stubbed by their postconditions; refinements propagate to callers; (3) CEx are not bug reports — multi-stage validation (reachability → callee feasibility → dynamic GCC replay → realism audit) distinguishes active vs latent/public-API vs modelling artifacts.
Specs inferred top-down from caller context + domain summary; dual-source generation (caller-intent vs impl-behavior) can flag disagreements for human review. Adaptive refinement (CEGAR-at-spec-level) with soundness guard; persistent spec store + pattern library.

VibeOS (~15k LOC C, LLM-assisted hobby kernel): 675 fns / 37 modules → 34 confirmed realistic findings out of 145 deduped CEx (16 confirmed_dynamic, 14 confirmed_system_entry, 4 confirmed_bmc); realism flagged 85 unrealistic + 26 uncertain (excluded).
Across corpora: 62 confirmed real bugs total — VibeOS 34; jq 1.8.1 → 2 GHSA filings; OOT Realtek r8125 → 1 CAP_NET_ADMIN MMIO R/W via u32 wrap; CCC (50k-LOC LLM Rust C-compiler, Kani) → 25 (24 panic-class + 1 functional-correctness on align_up).
Clean-verify on fuzzed surfaces: OpenSSL ASN.1 15/24 leaf clean; libxml2 pattern.c 54/54, xpointer 9/9, schematron 37/37; encoding.c 127 raw CBMC CEx → 0 confirmed after pipeline; curl strparse 8/20; protobuf upb 3/3.
Defaults: unwind k=4, per-fn timeout 120s; Rust unwind retry 4→16; inconclusive rather than block.

Harness shape: parse → call graph → domain summary → per-fn DSL specs (parser-gated) → LLM flag select (default-off on failure) → per-fn BMC → dedupe → 4-stage validate → refine+soundness-guard → persist knowledge.
Evidence tiers for Herdr-style reporting: dynamic / system-entry / BMC-only — don’t collapse to one “verified” bit.
Threat model framing required: LLM systems code often has safety implicit at call sites; reporting without active-vs-latent distinction over/under-reports.
Primary failure mode they admit: over-weak specs miss bugs silently (pipeline cannot self-detect); dual-source helps but doesn’t solve. Boundedness (k=4) misses deep-loop bugs.
Adopt: CBMC/Kani as DIY gate for C/Rust fleets; compositional per-fn harness; CEx realism pipeline; knowledge persistence across sweeps. Skip/ defer: treating bounded clean as unbounded FV; trusting LLM functional_spec without triangulation.
Code path: AProver/BMC-Agent — language-agnostic agent stages + per-backend adapters.

Authors call for quantitative precision/recall ablations + BMC-alone baselines (not yet). Spec-correctness is the trust bottleneck. Confidence high on architecture/patterns; medium on absolute bug counts as fleet benchmarks (single hobby kernel + selective OSS sweeps).