Agentic Model Checking
Youcheng Sun, Jiawen Liu, Daniel Kroening, Jason Xue

TL;DR
This paper introduces agentic model checking, a novel paradigm combining LLM agents with bounded model checking to verify system code, addressing the challenges of implicit specifications and bug detection.
Contribution
It presents a new verification approach that infers specifications, performs compositional checks, and refines based on counterexample validation, specifically tailored for LLM-generated code.
Findings
Confirmed real defects in LLM-generated kernel and compiler code
Produced bounded verifications on heavily-fuzzed code surfaces
Established functional equivalence on selected functions
Abstract
Verifying LLM-generated systems code is hard: bugs are prevalent, formal specifications are missing, and safety contracts are encoded implicitly at call sites rather than enforced at function boundaries. We propose agentic model checking, a paradigm that couples LLM agents with a bounded model checking backend under the principle agents propose, solvers verify: agents handle tasks requiring semantic judgment (spec inference, check selection, counterexample classification, refinement proposal) while BMC discharges every soundness-relevant decision. The paradigm rests on three commitments. Specifications are inferred top-down from caller context in a restricted DSL that translates deterministically into the backend's assume/assert primitives, with optional functional-correctness clauses lifting verification from panic-freeness to behavioural faithfulness. Verification is compositional:…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
