Technical Summary: Agentic Model Checking

Problem Statement

Verifying systems code generated by Large Language Models (LLMs) presents unique challenges that compound existing difficulties in formal verification. While LLMs can generate substantial bodies of code for operating systems, compilers, and drivers in languages like C and Rust, the resulting codebases often lack explicit formal specifications. Furthermore, safety contracts in LLM-generated code are frequently encoded implicitly at call sites rather than enforced at function boundaries.

This implicit encoding leads to a specific failure mode: helper functions (e.g., byte-indexing readers, offset arithmetic writers) often lack bounds and overflow guards, relying on the surrounding caller logic to maintain invariants. Consequently, the code functions correctly on well-formed input but fails on adversarial or crafted input. Traditional verification tools struggle here because they either over-report (flagging helpers as broken without context) or under-report (missing bugs because current callers do not trigger them). Additionally, existing LLM-based verification approaches often lack soundness for arithmetic and memory safety, while traditional deductive checkers struggle with the scale and loop-heavy nature of systems code and lack the ability to generate concrete counterexamples.

Methodology: Agentic Model Checking

The authors propose Agentic Model Checking, a verification paradigm that couples LLM agents with a bounded model checking (BMC) backend under the principle: "Agents propose, solvers verify."

The system, instantiated as BMC-Agent, operates through a pipeline where LLM agents handle tasks requiring semantic judgment, while a deterministic BMC backend (CBMC for C, Kani for Rust) discharges all soundness-relevant decisions.

Core Architectural Commitments

1. Top-Down Specification Inference:

   • Agents infer per-function preconditions and postconditions top-down from the caller context.
   • Specifications are generated in a restricted Domain Specific Language (DSL) that translates deterministically into the backend's native assume/assert primitives.
   • The system generates functional-correctness specs (e.g., reference-equivalence expressions, algebraic identities) in addition to defensive panic-freeness checks, lifting verification from mere crash avoidance to behavioral faithfulness.

2. Compositional Verification:

   • Verification is decomposed per function. Each function is checked in isolation against its inferred spec.
   • Called functions (callees) are replaced by stubs constrained by their postconditions. This implements an assume-guarantee discipline where a callee's postcondition becomes the assumption for the caller.
   • This approach prevents whole-program state explosion, allowing verification to scale with the size of a single function's state space rather than the entire program.

3. Multi-Stage Counterexample Validation:

   • BMC counterexamples are not treated as immediate bug reports. They pass through a rigorous validation pipeline to distinguish active in-tree crashes from latent failures or modeling artifacts:
     • Input Reachability: Propagating witness inputs up the call graph to determine if a caller can supply the values.
     • Callee Feasibility: Re-running BMC with real callee bodies to ensure the witness is reachable through real implementations.
     • Dynamic Replay: Compiling a harness to execute the witness on a host system, capturing signals (SIGSEGV, SIGABRT, etc.) to confirm dynamic crashes.
     • Realism Audit: An LLM agent reviews the full context (spec, harness, witness state) to classify the finding as realistic or unrealistic, filtering out framework-invariant artifacts (e.g., uninitialized globals, impossible hardware states).

4. Adaptive Refinement Loop (CEGAR at the Specification Level):

   • When a counterexample is classified as spurious (e.g., a loop-unwinding artifact), the system does not simply suppress it. Instead, an LLM proposes refinements (tightening preconditions, strengthening callee contracts, or adjusting solver parameters).
   • A soundness guard ensures these refinements do not mask real bugs.
   • Accepted refinements are persisted in a knowledge base (spec store and pattern library) and propagated to all callers, effectively extending CEGAR from predicate abstraction to the specification level with compositional propagation.

Key Contributions

The paper outlines six primary contributions:

1. Agentic Model Checking Paradigm: A framework where LLM agents manage semantic tasks (spec inference, check selection, classification) while BMC backends ensure soundness, enabling specification-free verification of LLM-generated C and Rust code.
2. Top-Down Specification Layer: A mechanism to infer per-function pre/postconditions and select semantically warranted arithmetic checks (e.g., overflow, pointer checks) via a DSL that translates to CBMC/Kani.
3. Compositional Verification Architecture: A scalable approach that checks functions in isolation under assume-guarantee contracts, parallelizing across call-graph layers.
4. Validation Pipeline: A four-stage process (reachability, feasibility, dynamic replay, realism audit) that categorizes findings into evidence tiers (e.g., "confirmed dynamic," "confirmed system entry").
5. Multi-Level Refinement Loop: A system that lifts CEGAR to the specification level, using spurious counterexamples to drive compositional refinements that persist across runs.
6. BMC-Agent Implementation & Evaluation: A working tool evaluated on diverse corpora, demonstrating the ability to confirm real defects, produce bounded clean verifications on fuzzed libraries, and prove functional equivalence.

Evaluation Results

The authors evaluated BMC-Agent on four corpora spanning C and Rust:

• VibeOS (C): A 15,000-line LLM-generated ARM64 kernel. BMC-Agent confirmed 34 realistic bugs across 12 modules. Of these, 16 were dynamically reproduced (SIGSEGV/SIGABRT), 14 were confirmed system-entry points, and 4 were formal model violations.
• Mature OSS Libraries (C): Evaluated on jq, OpenSSL, libcurl, libxml2, and protobuf upb. The tool disclosed 2 undefined-behavior defects in jq (filed as GHSA) and produced bounded clean verifications on heavily-fuzzed parser surfaces (e.g., 15/24 leaf functions in OpenSSL ASN.1 verified clean).
• Realtek r8125 Driver (C): Found a CAP_NET_ADMIN-gated MMIO bounds-check bypass in the rtl8125 tool ioctl, triggered by enabling specific overflow checks via the flag selector.
• claudes-c-compiler (Rust): A 50,000-line LLM-generated C compiler. BMC-Agent confirmed 25 real bugs, primarily panic-class defects on public-API byte helpers (slice OOB, integer overflows) and one functional-correctness violation. It also established bounded functional equivalence for ELF hash and header-write helpers.

Key Observations from Results:

• The precision of the tool is attributed to the realism-stage detectors (filtering framework artifacts), per-function flag selection (enabling checks default-off in standard configurations), and the feedback loop (converting recurring patterns into permanent invariants).
• In the Rust compiler case, the bugs followed a specific anti-pattern: the LLM wrote helper functions without boundary checks, relying on callers to maintain invariants. This resulted in code that worked on well-formed input but failed on adversarial input, a profile distinct from typical human-written compiler logic errors.

Significance and Claims

The paper claims that Agentic Model Checking addresses the "specification gap" in LLM-generated systems code by automating the inference of contracts and coupling them with sound, bounded model checking.

• Soundness vs. Scalability: By delegating soundness to BMC and using agents for semantic judgment, the approach avoids the unsoundness of pure LLM reasoning while overcoming the scalability limits of whole-program verification.
• Actionable Verification: The multi-stage validation pipeline ensures that reported bugs are not just theoretical counterexamples but are classified by their reachability and dynamic impact, distinguishing between active crashes and latent hardening tasks.
• Compositional Propagation: The system's ability to refine specifications and propagate them across the call graph allows it to learn from spurious counterexamples, improving verification quality over time without manual intervention.

The authors remain modest regarding future work, noting that broad quantitative evaluation (precision/recall at scale), deeper analysis of spec correctness assumptions, and cost reduction via token optimization are necessary next steps. They emphasize that the current results demonstrate the pipeline's capability to confirm defects and verify clean surfaces, but do not claim to have solved the general problem of verifying all LLM-generated code without limitations.