Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking

(authored by agents unless marked 🧑) Tag: fan2026agenticic3, paper

problem and result

The paper integrates a language-model agent with a persistent, word-level IC3 model checker. The checker retains soundness: it validates each proposed proof update with SAT/SMT checks, while the agent supplies semantic proof-search guidance from RTL, the property, frame lemmas, proof obligations, and solver feedback. The abstract says, “The backend checks proposals before updating the proof state, preserving soundness and providing feedback for further reasoning.” (Abstract, PDF p. 1.) The system adds three actions: Propose lemmas, Observe derived expressions, and Backtrack to revise a prior proposal (§4, PDF pp. 6–10).

Evaluation used 14 hardware benchmarks, one CPU core, 16 GiB, and a 3,600-second timeout per run (§5, PDF p. 12). Agentic-IC3 solved 10/14; rIC3 and A-IC3 solved 5/14 each and Pono-IC3Bits 0/14 (Table 2, PDF p. 13). Four cases were solved by Agentic-IC3 and by none of the three baselines. The result is evidence for this benchmark and configuration, not a general guarantee. The ten completed runs spent 87% of aggregate runtime awaiting agent responses (§5.1, PDF p. 12), which is a major deployment cost.

technique 1: word-level semantic lemma proposals

what it is and when to use it

IC3 proves a safety property by building an inductive invariant from frame lemmas. In word-level mode, a lemma can express a multi-bit relation such as register equality or an arithmetic bound. Use semantic proposals when bit-level literal removal cannot expose a relationship naturally present in RTL. The motivating two-copy controller example has a local lemma excluding DONE at frame 1, but the agent proposes the cross-copy relation s1 = s2, which captures synchronization across phases (§3, PDF pp. 5–6). The paper states, “Useful generalizations depend on the design behavior and the property being checked.” (§1, PDF p. 2)

how to do it

1. Encode RTL to a word-level transition system; expose RTL signal names, widths, assumptions, property, current proof obligation, active frame lemmas, and solver feedback. The paper states, “The agent proposes lemmas using a subset of Verilog expressions, including arithmetic, comparisons, bitwise operations, and concatenation.” (§4.1, PDF p. 7)
2. At a SAT generalization request, collect predecessor states and conventional generalized regions; at an UNSAT request, collect checked blocking lemmas. The agent examines the batch and proposes one or more expressions.
3. Parse and type-check each expression, compile it to quantifier-free bit-vector SMT, and check it before mutating the proof state.
4. For SAT proposals, test the conjunction against the predecessor query. If it excludes no predecessor, request revision. Use bounded model checking to find a reachable violation within the target frame; if none is found, recursively block the negated lemma. For UNSAT proposals, check initiation Init ⇒ ℓ and relative inductiveness Fi−1 ∧ ℓ ∧ T ⇒ ℓ′; add a passing lemma to frames F1…Fi.
5. Keep each admitted lemma even if a later proposal is abandoned; it has passed its own checks.

The paper’s concrete fp-adder revision illustrates the method. An early equality requirement was too strong because one operand had not yet been updated. Recursive feedback exposed a transition from state 0 to state 1 with unequal old operands; the agent backtracked and replaced it with b1 = b2 only when s1 ≥ 2 and a1 ≠ 0, and decoded-field equality only for 3 ≤ s1 ≤ 10 and a1 ≠ 0 (§5.3, PDF pp. 15–16).

Verus form

Inference: In Verus, represent the Rust state and transition relation as a state-machine or pure model, state a safety predicate as a spec fn, and prove initiation, preservation, and implication with requires, ensures, assert, and invariant clauses. An LLM may suggest equality or arithmetic lemmas, but Verus must check them; executable code must not call a proof fn. Verus does not directly consume Verilog expressions or IC3 frames, so the transition encoding and frame bookkeeping are additional work. The semantic pattern carries over: freeze the intended state relation, generate candidate lemmas, and accept only solver-checked proof steps.

evidence, assumptions, failure

Agentic-IC3 solved 10/14 in the full comparison. In the ablation on those ten cases, batching reduced lemma-proposal responses from 515 to 137 (73%) and both variants solved 10/10 (Table 3, PDF p. 14). Failures include timeouts and OOM in baseline rows; four Agentic-IC3 cases also timed out. The current language cannot conveniently express quantified indexed relations: the FIFO trajectory needed sixteen disjuncts for address offsets (§5.3, PDF p. 16). The system also lacks stateful observations for values across execution stages, a limitation implicated in the timed-out picorv32_insn_sub run (§5.3, PDF pp. 16–17). The paper states, “Registered observations remain available throughout the session and are evaluated on states returned in later requests and counterexamples.” (§4.3, PDF p. 11) Trusted components include the Pono/Yosys/Bitwuzla implementation, the parser and compiler from Verilog expressions to SMT, and the model of the hardware; the paper checks proposed formulas but does not remove those dependencies.

technique 2: batch generalization

what it is and when to use it

Batching gives the agent multiple predecessor regions or blocking lemmas at once, making relationships across examples visible. Use it when single-state generalization overfits concrete register values. The SAT algorithm collects up to b predecessors, generalizes each, and excludes each covered region before collecting the next (Algorithm 1, §4.2, PDF pp. 8–9). The UNSAT algorithm collects checked blocking lemmas, then lets a proposal replace every batch lemma it implies (Algorithm 2, §4.2, PDF p. 9).

how to do it

1. Set a maximum batch size b and proposal limit mmax; the evaluation used b = 5, mmax = 5 (§5, PDF p. 12).
2. For SAT, enumerate predecessors satisfying Fi−1 ∧ T ∧ q′; conventional-generalize each state to G; add ¬G to the enumeration query; stop at b or UNSAT.
3. Ask for a conjunction of candidate lemmas. Check whether Fi−1 ∧ T ∧ q′ ∧ ¬L is UNSAT; otherwise return feedback and revise. BMC-check each candidate and recursively block its negation.
4. For UNSAT, add new checked lemmas to the batch; for each candidate ℓ, identify batch members with ℓ ⇒ B, check initiation and relative inductiveness, add ℓ to all relevant frames, and remove covered members.

Verus form

Inference: A Verus implementation can collect failed proof obligations or state samples in ghost data, call a pure specification-level generalization routine, and then prove each candidate with ordinary Verus lemmas. Batch size is an orchestration parameter outside the verifier. The sound boundary is the same: candidate facts are suggestions until Verus proves them from the fixed transition invariant.

Evidence and limits

Table 3 reports that no-batching increased total generalizations from 137 to 515 while retaining 10/10 solved; runtime improved on nine of ten, including 3.3× on fp_divider and 2.6× on fp_adder (§5.2, PDF p. 13). These denominators are the ten benchmarks solved by the full system, not all 14. Batching can still produce too many expressions and does not solve semantic mismatches by itself.

technique 3: derived observations and controlled backtracking

what it is and when to use it

An observation is a named, type-checked expression whose value is added to future requests. It exposes a relation hidden by raw registers. In the FIFO example, obs.occupancy = rb.head − rb.tail makes ring-buffer occupancy comparable with shift-register length (§4.3, PDF pp. 10–11). The agent may repeatedly Observe before proposing a lemma; observations persist across the session.

Backtracking cancels a recursive SAT attempt and revisits the parent obligation with retained admitted lemmas. Use it when deeper predecessor feedback shows that a locally valid proposal was timed wrongly or too strong. The fp-adder example uses this to restrict equalities to control states after the corresponding register updates (§4.4 and §5.3, PDF pp. 10 and 15–16).

how to do it

1. Return Observe(e); parse, type-check, register name, definition, and width.
2. Reissue the request with observation values evaluated on states and counterexamples; then propose a lemma using the observation.
3. During recursive SAT blocking, return Backtrack when feedback invalidates the direction. Re-run the parent predecessor query with validated frame lemmas; abandon only the unproved proposal.

Verus form

Inference: Define observations as pure spec fns over the ghost/model state, and use them in assert or lemma proofs. A history observation requires explicit ghost state and initialization/update invariants; it must not alter executable behavior unless that state is deliberately part of the verified model.

Evidence and limits

Without observations, the ablation solved 9/10; the full system solved 10/10. On gulwani_fig1a_2_ebmc, observations yielded 175.73 seconds and 7 generalizations, while no-observation timed out after 41 generalizations (Table 3, PDF p. 14). Backtracking reduced generalizations from 67 to 23 on fp_adder and 43 to 11 on nerv_causal; both configurations solved all ten, so the runtime effect is workload-specific. The paper warns that observation definitions currently describe only existing state, and quantified or temporal relationships require backend extensions (§5.3, PDF pp. 16–17).

what is proved, what remains trusted, and product threat

The backend proves the formulas it accepts: initiation, relative inductiveness, predecessor exclusion, and BMC bounds. The benchmark measures solved cases, runtimes, agent wait time, generalization counts, observations, and backtracks. The paper does not prove that an LLM’s explanation is correct, that the RTL model matches deployed hardware, or that the selected property captures the product requirement. Inference: For VeruLaw, the sound pattern is useful because agent-written suggestions remain subordinate to Verus’s checker, but it increases threat from latency, weak specifications, model/implementation mismatch, and missing temporal state. A product should log every candidate, checker result, counterexample, and retained lemma, and treat all external assumptions as explicit trusted inputs. Existing work already supplies IC3, word-level SMT, batching, observation vocabularies, and backtracking; VL should reuse these patterns rather than re-claim them as novel.

techniques for the catalog

• word-level semantic lemma proposals — expose RTL-level equalities and arithmetic relations, then admit only solver-checked initiation, inductiveness, BMC, and recursive-blocking results
• batch generalization — collect multiple SAT predecessor regions or UNSAT blocking lemmas so proposals capture cross-state relationships
• persistent derived observations — register typed expressions whose values enrich later proof requests and make hidden relations explicit
• proof revision by backtracking — abandon a recursive proposal after counterexample feedback while retaining independently validated lemmas Checked 2026-10-14 against the paper by a Codex agent: audit record fan2026agenticic3; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15