Recoleta
GitHub
Source note

Agentic Model Checking

Authors
Youcheng Sun, Jiawen Liu, Daniel Kroening, Jason Xue
Source
arXiv
Published
Collection
Software Intelligence
Bounded Model CheckingCode VerificationLLM AgentsSystems SoftwareSpecification Inference
Open arXivMarkdown source

Summary

BMC-Agent verifies LLM-generated systems code by letting LLM agents write and refine specs while CBMC or Kani checks them. It targets low-level C and Rust bugs that need exhaustive bounded search and concrete counterexamples.

Problem

  • LLM-generated systems code often lacks formal specs and hides safety assumptions at call sites, so public APIs can crash on adversarial inputs.
  • LLM-only review can flag risky patterns, but it cannot prove absence of integer, pointer, bounds, or panic bugs across input ranges.
  • Plain bounded model checking needs specs and can produce counterexamples that may be unreachable or model artifacts, so findings need reachability and replay checks.

Approach

  • An LLM agent infers each function’s preconditions, postconditions, and optional functional-correctness checks from caller context and source code.
  • The inferred specs use a restricted DSL that maps directly to __CPROVER_assume and __CPROVER_assert for C, or kani::assume and kani::assert for Rust.
  • Each function is checked alone with CBMC or Kani; callees are replaced by stubs constrained by their postconditions.
  • A validation pipeline checks counterexamples through input reachability, callee feasibility, dynamic replay, and a realism audit before reporting bugs.
  • Unrealistic witnesses trigger spec or model refinements, which pass through a soundness guard before re-running the checker.

Results

  • On VibeOS, a 15,000 LoC LLM-generated ARM64 kernel in C, the paper claims 34 realistic bugs across 12 modules, with 16 reproduced as runtime faults.
  • On five mature OSS-Fuzz-hardened targets, jq, OpenSSL, libcurl, libxml2, and protobuf upb, it reports 2 undefined-behavior defects in jq and bounded clean verification on heavily fuzzed parser surfaces.
  • On an out-of-tree Realtek r8125 Linux driver, it reports 1 CAP_NET_ADMIN-gated MMIO bounds-check bypass in rtl8125_tool_ioctl.
  • On claudes-c-compiler, a 50,000-line LLM-generated Rust C compiler, it claims 25 real bugs: 24 panic-class defects on public-API byte helpers and 1 functional-correctness violation found by behavioral specs.
  • It also claims bounded functional equivalence for selected ELF hash and header-write helpers.
  • The default BMC settings include unwind bound k=4 and a 120 second per-function timeout, with Kani retries that raise unwind from 4 to 16 or shrink slice bounds from 4 to 2 to 1 when needed.

Link