KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked numbers against Tables 1, 2, 4, 5, 7 and the equations in Section 4.2, steps of all four techniques, quotations and Verus forms; corrected the source of the 3-of-232 mutant check (FormalBench, not this paper), removed an unsupported assumption about reference specifications, noted the second benchmark in RQ4, and marked unmarked inferences.

paper and scope

Wang and Sun present KBSpec, a retrieval and verifier-feedback system for generating JML specifications. It starts with official documentation, learns additional items from successful generation and repair trajectories, scores items by whether they help or harm verification, and retrieves the resulting memory for later programs. The experiments use OpenJML and Java; the Verus mapping is an inference. The paper reports no direct Rust or Verus implementation. A search of the research notes found no earlier walkthrough of this paper.

technique 1: dual-source specification knowledge base

what it is and when to use it

Seed a memory with external language documentation and examples, then add internal verifier-grounded experience. Use this when the specification language is low-resource and an LLM makes syntax or prover-compatibility mistakes that ordinary code pretraining does not teach.

how to do it

1. Collect official examples, tutorials, exercises, and expert repair guides.
2. Normalize each source into a knowledge item m_i={c_i,s_i,k_i} containing original content, an LLM-generated summary, and keywords.
3. Embed the program and the concatenation of each item’s content, summary, and keywords.
4. Retrieve the highest-similarity items and give them to the LLM while generating or repairing a specification.
5. Keep the specification itself subject to the formal verifier; retrieved text is advice, not evidence.

The paper says the two sources are “External knowledge collected from officially maintained online documentation” and “Internal knowledge collected by interacting with the formal verifier using LLM-generated specifications.” It reports that “The knowledge base evolves entirely through verifier feedback without modifying LLM parameters.”

Verus form (inference)

Build items from Verus documentation, verified examples, and accepted repair traces. Store the Rust snippet, Verus annotations, a concise summary, and keywords such as invariant, forall, decreases, or atomic. Retrieve by embedding the target function plus its current verifier error. Because documentation can be stale or wrong, compile every generated annotation with the pinned Verus version; retrieval cannot substitute for a proof.

evidence and limits

The initial JML base has 83 items: 11 examples, 31 tutorials, 26 exercises, and 15 repair guidelines. In final memories, internal items dominate; repair-derived items are the largest source. External documentation is therefore a seed, not the main long-term memory. Inference: the experiment does not test whether all retrieved rules are semantically correct independently of OpenJML.

technique 2: baseline-attribution and helpfulness credit

what it is and when to use it

Compare a knowledge-free generation with one generation using exactly one retrieved item. Credit an item when it changes verification from failure to success, penalize it when it changes success to failure, and mark all other outcomes neutral. This isolates which memory items are useful instead of treating every retrieved example as beneficial.

how to do it

1. Generate a baseline S_base=LLM(P) without retrieved knowledge.
2. Retrieve G items and generate one specification S_j=LLM(P,m_j) per item.
3. Verify every S_j and update item j: helpful if S_j passes while S_base fails; harmful if S_j fails while S_base passes; neutral otherwise.
4. Add successful generation trajectories to the candidate set for the next memory update.
5. At epoch end, rank old items by (helpful−harmful)/(helpful+harmful+neutral+10^-6) and keep the top L.
6. Add new successful items unless cosine similarity exceeds 0.95 with an existing item.

The attribution design is explicit: “This design makes each verification outcome attributable to a unique knowledge item.” The score is normalized because “neutral feedback reduces the magnitude of the score.”

Verus form (inference)

For each Verus memory item, run a paired trial from the same prompt and model seed: baseline annotation versus annotation augmented by one item. Verify both with the same Verus binary and timeout. Credit only changes in proof outcome, while separately recording whether the specification became weaker. Use a fixed hash of the target and seed to make attribution reproducible.

evidence, assumptions, and failure modes

Inference: credit measures marginal verifier success, not semantic usefulness or completeness, so a memory item can receive helpful credit by making a weak postcondition pass. The paper reports mutation-based completeness (Section 5.3.1), but the item score in Equation 7 does not include completeness. The paper’s own Table 7 lists weakening postconditions as a repair strategy in 33.0-51.2% of learned repair items (Section 5.5.2). Inference: similarity deduplication at 0.95 is a heuristic and can merge distinct rules.

technique 3: verifier-guided iterative repair with partial-progress credit

what it is and when to use it

When a generated specification fails, retrieve knowledge using both the current specification and its verifier error, repair it, and repeat. Partial credit rewards errors that disappear even when the final repair still fails. Use this for multi-obligation specifications where fixing one error reveals another.

how to do it

1. For each failed S_j, set S_j^(0)=S_j.
2. For up to three rounds, retrieve the single most relevant item using S_j^(t) and its error message.
3. Ask the LLM for S_j^(t+1), then verify it.
4. Represent each error report as a multiset E_t. Give partial progress p_t=|E_t−E_{t+1}|/|E_t|; track previously resolved errors H_t and regression penalty q_t=|H_t∩E_{t+1}|/max(|H_t|,1).
5. Credit terminal success against the no-knowledge baseline; for two failures, add (p_t,q_t,1−p_t) to the helpful/harmful/neutral totals. Treat unextractable timeout/internal errors as neutral when the baseline also fails and harmful when the baseline succeeds.
6. Store successful repair trajectories in the candidate memory.

The paper states: “For each initially failed specification S_j, we set S_j^(0)=S_j and perform at most three repair rounds.” It defines partial progress as a ratio that “rewards only error instances that disappear after the repair.”

Verus form (inference)

Parse Verus diagnostics into stable categories such as failed invariant, trigger, arithmetic lemma, ownership, unsupported syntax, and timeout. Retrieve a single rule with the current code and diagnostic, apply at most three repair attempts, and rerun Verus. A disappeared diagnostic is useful feedback, but only a final successful proof establishes correctness. Preserve the original specification so that weakening a postcondition can be detected rather than silently rewarded.

evidence and limits

Ablation shows iterative repair is one of the strongest components: removing it lowers C@All by 21.82, 17.22, and 13.33 percentage points for GPT-5.2, GPT-5-mini, and Claude-Sonnet-5. Removing partial repair credit lowers C@All by 1.53–3.40 points. Error taxonomy shows loop reasoning failures at 16.6–24.0% and arithmetic failures at 14.7–22.5% of learned repair items, but these categories were assigned by a keyword matching approach over item content and summary (Section 5.5.2, Table 7), which the paper does not validate against a semantic classifier.

technique 4: knowledge-augmented inference and completeness measurement

At evaluation time, freeze the memory and retrieve the top three items for the program. On each repair round, retrieve again using the current specification and error message. The benchmark has 699 FormalBench-Base Java programs; training samples 100 of 1,794 diverse programs per epoch for up to ten epochs, with early stopping after two epochs without pass-rate improvement. OpenJML 21 is the verifier and the retriever is all-minilm-l6-v2; training uses G=5 items per separate rollout.

KBSpec’s pass rates are 73.96% (GPT-5.2), 47.35% (GPT-5-mini), and 62.66% (Claude-Sonnet-5), versus SpecGen’s 41.63%, 28.18%, and 47.93%. C@All is 38.51%, 30.92%, and 39.46%, while C@Pass is lower than SpecGen on all three backends. C@Pass uses mutation testing: generate K non-equivalent mutants and compute the fraction that the specification rejects; C@All assigns zero completeness to programs without a passing specification. The paper notes PR+FR<1 because timeouts and internal verifier errors are additional outcomes.

Verus form (inference)

Use a frozen catalog during product evaluation. Retrieve top-k rules for initial generation and for each verifier repair. Measure pass rate and mutation-based completeness of Rust specifications, including cases with no passing proof. Mutants must preserve compilation and violate the intended contract; otherwise completeness is meaningless. Record denominators for attempted programs, verifier passes, timeouts, and internal errors separately.

what is proved, trusted, and threatening to VL

The paper measures OpenJML verification outcomes and mutation-based completeness, not proof soundness beyond OpenJML’s trusted implementation. Its completeness metric relies on mutants being non-equivalent; the paper cites FormalBench [10] for a manual inspection that found only 3 of 232 mutants (1.3%) equivalent after Equivalent Mutant Suppression (Section 5.2.3), not a check of its own. It reports contradictions transparently: KBSpec raises pass coverage but lowers C@Pass versus SpecGen, while C@All rises because more programs receive some verifiable specification. Inference: external validity is limited to Java/JML and three LLM backends. The paper also runs a frozen knowledge base on SpecGenBench, 120 programs, where KBSpec has a higher PR and C@All than SpecGen on all three backends (RQ4, Table 8).

VL should not redo generic retrieval-augmented prompting. The reusable pieces are verifier-attributed item scoring, partial-error credit, similarity deduplication, and freeze-before-evaluation discipline. The threat to agent-written verified Rust is high for specification omission: a memory can teach the agent to weaken postconditions or remove difficult quantifiers until Verus passes. The agent must therefore track contract strength and run mutation or adversarial tests in addition to proof checking. This threat statement is an inference from the paper’s explicit completeness tradeoff and repair taxonomy.

techniques for the catalog

• dual-source evolving knowledge base — seed memory from official specification material and grow it from verifier-accepted generation and repair traces
• baseline-attributed helpfulness scoring — credit or penalize one retrieved item by comparing its verifier outcome with a knowledge-free baseline
• partial-progress repair memory — retrieve on code plus diagnostics, iterate repairs, and score disappeared and recurring error obligations
• frozen retrieval with mutation completeness — evaluate retrieved specification generation with pass rate, fail rate, and completeness over non-equivalent mutants

Last edited: 2026-10-13