tools-verify-kani-with-properties

Frozen 2026-10-09. This skill moved to ai-native-storage-workbench (fv/skills/). Edit it there; this copy is not updated. Install the current version with fv/install.sh <this-repo>.

Scope (2026-10-04): prove only LEVEL-2 properties. Skip every id listed in the bundle's level2_excluded: (written by gate/level1.py): those are spec<->code discordances, reported in discordances.yaml and NOT formally verified — proving them only rediscovers a disagreement the reconciliation already found. Also skip any hazard-worded record. "Attempt every property" below means every level-2 property.

Prove under the level-1 assumptions. If the bundle has level2_assumptions:, each entry is an input range the specification and the code disagree on (discordances.yaml, kind input range mismatch). State its assume_rust as a precondition on the entry operation's input (Creusot: #[requires(...)] on the driver; Kani: kani::assume(...) before the call), and record which ones a proof uses in its advisory note (assumes: [D-RANGE-…]). Add NO other precondition that the obligation does not state: the gate rejects a proof that assumes more than its base.

Goal

Verify a component with Kani and record exactly what was verified. Inputs are the component's spec (the intended behavior) and its Rust code (functions + interface). Outputs are (1) the #[cfg(kani)] mod verification harnesses and (2) the per-property status/symbol/fidelity/evidence written back into the shared unified_properties.yaml under each property's kani: block.

This skill = tools-verify-kani + explicit spec pairing + a status-write-back step. Use tools-verify-kani for the create mechanics (stub unsafe/FFI, kani::assume mirroring production guards, run/fix, its "core rule"). This skill adds spec-derived contracts and the structured write-back into unified_properties.yaml.

Steps

0. Environment — confirm the toolchain FIRST (mandatory). Confirm cargo kani is reachable and run from the component directory, not the workspace root — the root triggers a spurious gpu-services feature error that is an environment artifact, never a property verdict. A missing/erroring toolchain is a blocker to fix or escalate here, never a tool-boundary and never a reason to leave a property unattempted:

   command -v cargo-kani >/dev/null || { echo "FATAL: cargo-kani unreachable — escalate to user"; exit 1; }
   cargo kani --version    # expect a version line, not an error
   cd components/<name>    # run all `cargo kani` from HERE, not the workspace root
   

1. Resolve inputs — consume the inventory, do NOT re-extract. Load the property inventory verif/unified_properties.yaml (Role 1, build-property-inventory): the agreed, id-keyed, tool-independent property set. Also open the Rust functions + interface (src/**, interfaces/); use the spec only for an obligation's wording, never to mint a new one. Do not build a private per-tool property list. If the inventory is missing, stop and run build-property-inventory first. If you spot a real obligation the inventory lacks, flag it back to the inventory so it gets an id.
2. Harness the shared/global invariants FIRST, once — then reuse. Before per-method work, take the inventory properties whose bundle spans multiple methods (the inventory marks these as global / maintained invariants with an attachment count). Order by attachment count, highest first. Prove each as a single inductive harness: build a symbolic valid state, kani::assume(inv(state)), call the mutator, assert!(inv(state')) — plus one establishment harness (initialize from scratch → assert!(inv)). Record it under its one inventory id; its status then propagates to every bundle automatically (Role 3 attaches by id — do NOT re-harness it per method, and do NOT skip it because "no single method owns it"). One cheap invariant harness unblocks every method in its bundle at once.
3. Then, for each remaining per-method obligation, harness the CODE against it. Function granularity, using the obligation from its inventory row (id, statement, kind): kani::assume(<precondition — mirror the production guard>) → call the real function → assert!(<postcondition>), taking the already-proved invariants as assumed pre-state. Never lift a statement into the harness.
4. Run. cargo kani to green; fix gaps; audit that each assume matches a real production guard (no over-assuming that would make the proof vacuous).
5. Validate (anti-vacuity). Fault-inject (a contract-violating change) and confirm the harness FAILS; if it still passes, it isn't bound to the real code — fix it. Then revert. For a maintained invariant, also fault-inject a mutator that breaks it and confirm the inductive harness FAILS. (--harness substring-matches; use --exact with module::name to run one in isolation.)
6. Produce artifacts the scorer can reproduce — you do NOT write your own status. The verdict is assigned in Step 7 by the shipped scorer, which runs your harnesses. Your job in Step 6 is to leave, for every property, a runnable artifact named so the scorer finds it:
   • One harness per property id, named verify_<id> (id lowercased, -→_). If a single descriptive harness covers a property, point the scorer at it with kani.evidence.harness: <name> instead — but it must exist and pass on its own.
   • For any property you cannot prove on the first clean attempt, build the lever-battery variants that gate/lever_battery_kani.yaml requires for the failure class you hit — as named runnable harnesses: verify_<id>__nounwindcheck, verify_<id>__concrete, verify_<id>__split_*, verify_<id>__stub. A tool-boundary is inadmissible until every required variant exists and the scorer has run each — a missing variant scores UNRESOLVED (gate fails), not tool-boundary.
   • An anti-vacuity twin verify_<id>__mutant wherever the property could pass vacuously — a deliberately contract-violating copy that the scorer requires to FAIL.
   • In unified_properties.yaml under the kani: block you may fill only the advisory fields the scorer does not own: fidelity (real-type-bounded | representative | arithmetic-core | bounded-shallow) and a human note; and for a genuine cross-component delegation, a resolvable delegate_to: (named component + concrete obligation). Do NOT write status, symbol, or evidence — the scorer overwrites them from the live run and stamps _scored_by: scorer_kani. Anything you type there is discarded; the only way to move a property's status is to make its artifact reproduce. fidelity meanings: real-type-bounded = real product type/code under a stated #[kani::unwind(N)] (a bounded proof is a real proof); representative = the ∀ shrunk to one symbolic representative; arithmetic-core = an extracted arithmetic core behind a stub (★); bounded-shallow = a pass under --no-unwinding-checks at low unwind — every loop cut at N, sound only for executions where each loop runs ≤N (disclose the cut in note; route a fully-sound proof of the same obligation to Creusot).
7. Gate — the shipped scorer decides, by reproduction (mandatory; you cannot grade yourself). The reproduction gate is scorer_kani.py, which the component-verify orchestrator runs in its Step 2.5. If you are running this skill standalone, invoke it yourself before returning and paste its output into your report:

   python3 "$(git rev-parse --show-toplevel)/.claude/skills/component-verify/gate/scorer_kani.py" \
       components/<name>/verif --component-dir components/<name> --cap-seconds <cap>
   

   The scorer executes each verify_<id> harness (rebuilding from source, so a hand-edited artifact cannot fake a pass), captures wall-clock + peak RSS from the run, checks the anti-vacuity mutant, and writes the scorer-owned status/evidence/note/_scored_by. It assigns proved / tool-boundary (only after the full lever battery ran and the residual signature is not a known defeat) / delegated (resolvable referent) / UNRESOLVED (no harness, an unreproducible pass, a missing required lever variant, a known-defeat signature, or a broken harness) — and exits non-zero if any verifiable property is UNRESOLVED. If it exits non-zero you are not done: for each UNRESOLVED id, produce the missing harness / the demanded lever variant / fix the broken harness, and re-run the scorer. Iterate until it exits 0. You may not hand back the run, write a "partial run" summary, or ask the user to accept the remainder while the scorer fails — no matter how many properties are proved. Editing the YAML to say proved does nothing: the scorer reproduces from source and overwrites it.

Coverage discipline (mandatory)

Attempt every property in the inventory that you can express as a harness. You do not get to pick lanes here — routing properties across tools is a separate step, not this one. Your job is to verify or fail trying, and to record the outcome keyed to the inventory id so Role 3 can aggregate it.

• No pre-filtering by lane, effort, or budget. "Better suited to Creusot", "intractable", "requires induction", "to stay within budget" are not acceptable reasons to omit a property. If you can write the harness, run it.
• Attack the highest-leverage properties first. A property in many bundles is higher priority, not lower, because one inductive harness discharges it everywhere. Harness the shared/global invariants (ordered by attachment count) before method-specific obligations; a cheap invariant left at not_yet silently keeps every method in its bundle unproved.
• Attempt at a tractable bounded geometry. Kani proves exhaustively at the chosen size: pick a small #[kani::unwind(N)] and a small structure that still exercises the property, and use kani::stub to replace unsupported/FFI dependencies rather than dropping the harness. A bounded proof is a real proof — report its geometry.
• Bounded effort, not infinite grind. Give each harness a real attempt against a stated cap (per-harness CBMC timeout). Exceeding the cap converts the property to a tool-boundary with the timeout signature (miss_class: TOOL, note: the exact >N min at unwind=K string) — it does not license leaving the property unattempted. The cap decides when the captured signature is ready for the scorer, never whether you may skip.
• Every non-success carries a reproducible signature, never a subjective verdict: VERIFICATION FAILED, an unwinding-assertion failure (N too small), unsupported_construct: <name> (e.g. _xgetbv from crc32fast), or a SAT/solver timeout (>N min at unwind=K). Ban bare "intractable"/"out of scope".
• Only two legitimate non-proofs, each needing a one-line technical reason and a suggested route: (a) Not expressible for a bounded checker — concurrency interleavings, liveness/timing, or a property that only holds at unbounded scale and no finite geometry witnesses it; (b) Depends on effects Kani cannot model — real I/O, hardware, FFI (and no stub is faithful). Everything else must be attempted at a bounded geometry and reported with its signature under bucket (a).
• Concrete string/char CONTENT is EXPRESSIBLE here — prove it, do not claim a boundary. A property Creusot cannot state because its string view is opaque (contains a tag, equals "ERROR", ends in '\n', excludes an ESC byte, or is built by format!) is exactly what a bounded checker CAN witness on the concrete bytes. When unified_properties.yaml shows such a property with creusot.claims_inexpressible and covered_by: kani, that is your obligation to discharge bounded (small symbolic representative, real type), not to punt. There is no inexpressibility hatch for Kani in this pipeline — bounded byte reasoning is Kani's home turf, so a Kani inexpressibility claim on strings is illegitimate.

Coverage-extending levers — exhaust these BEFORE recording ⊘ (mandatory)

A "tool boundary" is only legitimate after the applicable levers below have been tried and shown to fail with a captured signature. A wall that a documented lever clears is a recipe gap, not a tool boundary — recording ⊘ without trying the lever is a false negative (this is exactly how a HashMap-backed component was once mis-recorded as whole-component ⊘ when a one-line stub proved it in 3.5 s). Enable unstable levers with the matching -Z flag: cargo kani -Z stubbing, -Z function-contracts, -Z loop-contracts.

• HashMap / HashSet construction wall (RandomState::new → getrandom → syscall). This is DEFEATABLE, not a boundary. Stub RandomState::new with a deterministic seed and construct the real type in situ:

  use std::collections::hash_map::RandomState;
  use std::mem::{size_of, size_of_val, transmute};
  fn concrete_state() -> RandomState {
      let keys: [u64; 2] = [0, 0];
      assert_eq!(size_of_val(&keys), size_of::<RandomState>());
      unsafe { transmute(keys) }              // fixed [0,0] seed, no syscall
  }
  #[kani::proof]
  #[kani::stub(RandomState::new, concrete_state)]   // also covers the Default path
  #[kani::unwind(5)] #[kani::solver(minisat)]
  fn harness() { /* build + drive the real HashMap-backed struct */ }
  

  Fidelity real-type-bounded (the real product type, in situ; symbol ✓). Two measured caveats: (a) use concrete representative keys — symbolic keys (kani::any()) drive SipHash over symbolic bytes and blow up hashbrown's probe loop (record such a harness as representative fidelity, not a boundary); (b) the seed stub is sound only for map semantics (insert/get/remove/len/containment) — never assert anything depending on hasher randomness (iteration order, DoS-resistance) under it.
• extern "C" / FFI in the path. #[kani::stub(the_extern_fn, rust_model)] replaces the foreign fn with a Rust model (symbol ★, disclosed in note). Or give it a contract and #[kani::stub_verified] (-Z function-contracts). Only ⊘ if no faithful model exists.
• Unbounded loop. Prefer #[kani::loop_invariant(..)] (+ #[kani::loop_decreases(..)], -Z loop-contracts) over an ever-growing #[kani::unwind] — an inductive invariant removes the bound. (Not while let loops; decreases is integer-only.)
• Large / slow formula. Switch #[kani::solver(minisat|kissat|cadical|z3)] (minisat cleared the hashbrown swap_nonoverlapping loop here); bound symbolic state with kani::assume; decompose a huge function via #[kani::proof_for_contract] + #[kani::stub_verified] so callers assume the verified contract instead of inlining the body.
• Sweep the unwind number — and use --no-unwinding-checks for shallow coverage (the coverage-over-depth lever). A single fixed unwind is a trap: too low raises a spurious unwinding assertion loop N FAILED (not a real defect — just "the bound is below the loop"), too high explodes the SAT formula into a timeout. Iterate the bound — try --unwind 2,3,4,5,… (cheapest first) and take the smallest that reaches the property without an unwinding failure; record the winning N in evidence.unwind. When the loop genuinely needs many iterations to terminate (e.g. hashbrown's probe loop) and the sound geometry times out, add --no-unwinding-checks: Kani then cuts every loop at the unwind bound and verifies the bounded prefix, turning a >500 s timeout into a ~7 s pass (measured ~70× on the ≥2-HashMap-mutation harnesses here — unwind 5 timed out >500 s under minisat and cadical; unwind 2 + --no-unwinding-checks passed in ~7 s / ~355 MB). Soundness cost — record it honestly: this is bounded-shallow fidelity (symbol ✓, but the note must state "loops cut at N; sound only for executions where every loop runs ≤N times; deeper iterations out of scope"). It is coverage over depth: it lets you sweep many functions cheaply and confirm the shallow slice, but it is not a full proof — route a fully-sound proof of the same obligation to Creusot (FMap induction removes the bound entirely). Prefer real levers (loop contracts, solver switch, smaller symbolic state) when they fit in budget; reach for --no-unwinding-checks to widen coverage across source, not to replace a sound proof where one is affordable.
• Reference: verif/skills_research/KANI_capability_catalog.md in the eviction-policy-session-lists component carries the full catalog with flags, examples, and soundness costs.

Harness hygiene the GATE depends on — measured, not theoretical (mandatory)

🔴 Do NOT generate harnesses with macro_rules! — the gate cannot see them

find_harness_names discovers harnesses by regex over source text. A harness emitted from a macro is invisible to it, so the property scores "no runnable harness" while the harness sits in the file — blaming you for a discovery limitation. Measured: 13 global-invariant harnesses written via macro_rules! would all have scored that way. Write explicit #[kani::proof] fn verify_<id>() functions, however repetitive.

🥇 LOOP CONTRACTS FIRST — the correct answer to a loop that will not fit a bound

-Z loop-contracts replaces unrolling with a Floyd–Hoare invariant, so the loop body executes exactly twice and verification cost is decoupled from the iteration count. This is available in cargo-kani 0.67.0 (checked: -Z accepts loop-contracts, function-contracts, quantifiers, ghost-state, mem-predicates, uninit-checks, valid-value-checks).

Measured, on a 1024-iteration loop that mirrors a real component's halve():

approach	base harness	its mutant (MUST fail)	time	sound?
--unwind 4 --no-unwinding-checks	SUCCESSFUL	SUCCESSFUL	0.034 s	NO — vacuous
-Z loop-contracts, no bound at all	SUCCESSFUL	FAILED ✓	0.20 s	YES

Read that table before reaching for --no-unwinding-checks again. The bounded version "verified" in 34 ms and so did a harness asserting the exact opposite, because a 4-iteration bound over a 4096-iteration loop prunes away every path the obligation is about. The loop-contract version costs 6× more and is worth infinitely more: it holds for all iteration counts, and its mutant correctly fails. Kani's own tool paper puts the same contrast at 0.2 s with a contract versus 91.8 s unrolling 19 iterations.

#![cfg_attr(kani, feature(stmt_expr_attributes, proc_macro_hygiene))]
let mut i = 0usize;
#[kani::loop_invariant(i <= COLS && (i == 0 || c[0] <= 127))]
while i < COLS { c[i] >>= 1; i += 1; }

Run with -Z loop-contracts. Companions: #[kani::loop_modifies(...)] when the inferred write set is wrong, and #[kani::loop_decreases(expr)] for termination.

Limitations you WILL hit, so design around them:

• An invariant that is not INDUCTIVE fails even though it is true. This is the trap, and it looks exactly like a tool bug. CBMC havocs the loop's write set, so the invariant must be re-establishable from itself plus the body — not merely true of the final state. Measured: a[0] <= 127 after a[i] >>= 1 is inductive for u8 (halving can never exceed 127) but NOT for u64, and the u64 version fails while being perfectly true. An earlier version of this section blamed kani #3168 (struct field projections) for that failure. That was a misdiagnosis and #3168 does NOT reproduce on 0.67.0 — invariants over a struct field (s.a[0]), a &mut array parameter, a by-value array parameter and a harness-body local all prove. So do not hoist state out of structs to appease the tool; check inductiveness first. When an invariant fails, ask "could the body break this from a state satisfying it?" before suspecting Kani.
• Loop contracts do not havoc state the loop only reads, so a read-only scan over an assumed-well-formed structure needs no loop_modifies.
• while let loops are unsupported. while and loop work; for works over ranges, slices, Vec, Iter and the common adaptors.
• Without loop_decreases you get PARTIAL correctness — "if the loop terminates, the result is correct". Kani's docs show an infinite while true whose post-loop assertion is reported proved. So an invariant alone does not rule out non-termination; add a decreases measure when that matters, and record fidelity accordingly.
• loop_decreases takes integer expressions only, no lexicographic tuples, no field projections, and it conflicts with loop_modifies in this version.
• The invariant and the decreases expression must be pure; side effects there are unchecked and "could lead to an unsound proof result".
• Diagnosing: establishment fails → invariant too strong for the initial state; preservation fails → too weak to prove itself, or too strong for the body; post-loop assertion fails → invariant plus !guard is not enough.

🔴🔴 kani::forall! SILENTLY DROPS a body containing && — the worst trap found so far

Under -Z quantifiers, measured shape by shape on 0.67.0:

body	binds?
a[i] == 42 · b[i] · b[i] == c[i] · a[i] <= d[i] · a[i] != s	✓
(b[i]==false) || (a[i]==42) · 3-way || over struct fields	✓
(b[i]==true) && (a[i]==42)	SILENTLY IGNORED

The assume compiles, runs, and constrains nothing. Also silently ignored: a symbolic upper bound (only constant bounds bind). Related: \|i: T in ..\| is a parse error, and a body indexing through a reference can fail type inference — wrap it in fn pred(p: &Pool, i: usize) -> bool.

Know which direction is dangerous. A dropped forall! inside an assume only weakens the precondition, so the proof gets harder and never vacuous. A dropped conjunct inside an assertion or a loop invariant is straight vacuity, and no tool flags it — not Kani, not our mutant twins necessarily, because the mutant may be dropped the same way.

Rules, mandatory wherever -Z quantifiers is used:

1. Never put && inside forall!. One forall! per conjunct.
2. Only constant upper bounds.
3. Carry a check_assumes_actually_bind harness that re-asserts every assumed predicate at a symbolic index. If an assume silently dropped, that harness fails and tells you so. This is cheap (measured 5.08 s) and it is the only mechanism that catches the failure at all.

🔴 A STUB CAN BLIND THE CODE — a vacuity source no mutant twin catches

Stubbing a container to make a harness affordable can silently remove the behaviour under test, and then the property AND its mutant both pass. Proved, not theorised: with BTreeSet stubbed on eviction-policy-session-lists, a diagnostic harness asserting p.leaves.len() == 2 && p.evict_oldest().is_none() PASSES — the model holds two leaves while the operation that selects a victim returns None, because the read path (leaves.iter().next()) was never intercepted.

Every obligation phrased as an implication over a returned value ("if a victim is returned it is a leaf", "a protected block is never chosen") is then vacuously true, and its mutant is vacuous for the same reason, so anti-vacuity cannot see it. Applied carelessly, stubbing is worse than the bounded harnesses it replaces.

Required whenever you stub: a diagnostic harness asserting the stubbed path is still REACHED and still returns something — the analogue of check_assumes_actually_bind. If the operation can return "nothing" while the state says otherwise, every downstream implication is worthless.

Also know what Kani will and will not let you stub, measured on 0.67.0:

• A stub must repeat the target's generics exactly; a monomorphised stub is rejected ("mismatch in the number of generic parameters"). So a stub cannot own typed state, which forces a type-erased side table if you need per-instance state.
• External-crate trait impls cannot be stubbed at all: btree_set::Iter::next → "unable to find next inside struct"; <Iter<'_,T> as Iterator>::next → "unable to find implementation of associated function". So any obligation whose only read path is an iterator is out by construction.
• Per-instance stub state keyed on the receiver address works, but a Rust move relocates the struct and orphans the table — so the object must be built in place and never moved. A Vec<Mutex<Pool>> therefore cannot use the technique at all.

The CAPACITY-SCALING check — a second, independent test that a proof is real

The mutant twin catches a proof with no content. It does not catch a proof whose bound merely happened to be generous enough for the states the harness explores. So for any harness over a fixed-capacity structure, re-run it at a larger capacity and require every verdict to hold.

Measured on a 474-line Pool model, 7 harnesses, capacity 8 → 32 (a 4× arena), same source, same flags:

	CAP=8	CAP=32
3 base proofs	19.1 / 25.6 / 23.9 s, all SUCCESSFUL	139.7 / 130.9 / 74.0 s, all still SUCCESSFUL
3 mutant twins	all FAILED (correct)	all still FAILED
assume-binding guard	5.1 s	20.9 s
undetermined checks	0	0

No verdict flipped and nothing became undetermined at 4× the state space. That is the signature of a real proof. A harness leaning on a lucky bound behaves the opposite way: checks start coming back undetermined as the space grows, because the solver can no longer reach them.

Cost grew ~CAP^1.5–2.6 — with the data size, not with loop trip count, which is exactly the property loop contracts are supposed to buy and is the cleanest evidence that they delivered it.

Use it as a gate-time discipline: prove at the working capacity, then re-run the property and its mutant at 2–4× and require both verdicts unchanged. It costs one extra run per property and it closes a hole the mutant twin cannot see.

Skolemise instead of quantifying — measured 400× cheaper

For a scan loop, replace a universally-quantified invariant with a witness index chosen symbolically BEFORE the loop and referenced only inside the invariant. The proof then holds for an arbitrary witness, hence for all of them, and stays quantifier-free. Measured on the same obligation: 1120 s with a real forall! vs 2.81 s Skolemised. It does not work for permutation loops (a shift-insert moves values between cells, so a single witness is not inductive). Those need a real forall! at ~1120 s per harness — not viable at scale, so prefer a model that avoids permutation loops entirely.

The escalation order for a loop-bound failure — strongest claim first

1. #[kani::unwind(n)] / --unwind n sweep with unwinding checks ON. Anything that proves here is full strength. Note Kani needs the bound one more than the iteration count, and break/ continue can need two or three more.
2. -Z loop-contracts. Unbounded and full strength. Prefer this over any bounded fallback.
3. Shrink the problem — a smaller const bound in the harness, honestly recorded, so the claim is about the smaller structure rather than silently about nothing.
4. --no-unwinding-checks LAST, and never without its mutant twin. See below.

🔴 --no-unwinding-checks PRUNES paths — and it destroys Kani's own completeness claim

Kani's guarantee is stated as "practically complete when all unwinding assertions pass". The unwinding assertion is the check that your bound was big enough. --no-unwinding-checks deletes exactly that check, so it does not merely narrow the claim — it removes the evidence that the claim covers anything. Kani's documentation never recommends the flag; the tutorial's remedy for a too-small bound is to raise the bound or shrink the problem.

🔴 --no-unwinding-checks PRUNES paths — it does not merely truncate them

So a harness can pass with no content. Measured on eviction-policy-session-lists: in the first full run every verify_* passed AND 36 __mutant twins passed too, and a passing mutant is the definition of a vacuous proof. Two consequences you must design for:

1. bounded-shallow is the fidelity where vacuity is most likely, not least. Write the harness so that no reachable loop needs more than the bound, and say so in the note. The scorer now re-runs the mutant under the same flags as the proof, so a contentless bounded pass is caught — but a harness written to be honest is better than one caught being dishonest.
2. For a refutation, bind the outcome instead of trusting a bare assert. A pruned pass would score a real defect as proved. The idiom that survives pruning: bind the outcome, kani::cover! the violating case, then assert. An unsatisfiable cover is a FAILED check, so the harness fails whether the violation is unreachable OR the path was pruned away — it can never pass silently.

Why every proof here carries a mutant twin — Kani has no vacuity detection

Kani's own tool paper is explicit that a bad assumption "makes the proof vacuously true, so assumptions must be reviewed as carefully as the code itself", and it describes no vacuity detection, no reachability or coverage metric, and no assumption-consistency check. Mutation testing of proofs appears nowhere in it. So the verify_<id>__mutant twin is not ceremony and not duplication: it is the only mechanism in this pipeline that can tell a proof from an empty one, and the tool cannot do it for you.

Measured worth: on eviction-policy-session-lists the gate found 52 of 90 harnesses vacuous, and on eviction-policy-optimized one published proof was empty. Every one of those passed Kani cleanly.

Trusted stubs make a proof CONDITIONAL — prefer stub_verified

A plain #[kani::stub(f, g)] is not checked against the real f. Any result that depends on it is sound only if the stub over-approximates faithfully, which nothing verifies. With -Z function-contracts you can instead give f a contract, prove it once with #[kani::proof_for_contract], and use stub_verified — then the abstraction is checked rather than trusted. Where you must use a plain stub (the RandomState::new seed stub is the standing example), record fidelity: representative and name the stub in the note, so the page shows a conditional claim as conditional.

Solver choice is a real lever, and wider than two options

Backends available: SAT — MiniSat (default), Kissat, CaDiCaL; SMT — Z3, cvc5, Bitwuzla. Their timeout profiles differ sharply, so a sat-timeout is worth retrying across several, not just one swap. Quantifiers are bounded: SAT backends expand eagerly and warn above ~1000 values, while SMT backends accept runtime-valued bounds — so a quantified invariant over a large array wants an SMT backend.

--harness NAME matches SUBSTRINGS

One flag can run several harnesses and interleave their verdicts. Never infer a verdict for one harness from a run that matched others, and avoid names that are prefixes of other names. This produced a false proved on a property that both tools had in fact refuted — the worst bug this pipeline has had.

Write a discriminator wherever you suspect a missing check

A variant that PASSES once the suspected check is added isolates the cause to that check alone. On eviction-policy-optimized that was the single strongest piece of evidence in the whole report, and it is what turns "this assertion failed" into "this specific missing bounds check is the defect".

Definition of done — "not attempted" is not an outcome (mandatory)

Every inventory property must reach exactly one of three end states. There is no fourth box.

1. Proved — a passing harness (bounded scope stated), or a disclosed faithful stub/mirror with the boundary named.
2. Delegated — the obligation is owned by a different component across a real interface boundary; name it and route it. "Belongs to another tool" is not delegation — that is still your property to attempt here.
3. Tool boundary hit — you exhausted the applicable coverage-extending levers, wrote the harness, ran it, and captured a reproducible failure signature (unwinding-assertion / unsupported_construct: <name> / SAT-timeout >N min at unwind=K). Evidence is mandatory; a limit asserted without a run, or before trying the lever that clears it (e.g. the RandomState stub for a HashMap wall), is not a legitimate boundary — it is a recipe gap.

"Harness not written" / "authorable but not done" is NOT an end state. A property with no harness is unfinished work, never a rating. Do not report it, do not park it, do not hand back the run with it open. The only exit from the not-done set is an actual attempt, which forces the property to (1) or (3). On uncertainty the default is attempt, never "tool limitation." A run returned with unattempted properties has not met the bar, no matter how many were proved.

An unattempted property — no runnable harness produced — is a transient working state, never returnable. It means the work is unfinished, not that a boundary was found. You do not write status at all (Step 6); enforcement is by reproduction, not by reading a field you set. The gate (Step 7) is the shipped scorer_kani.py: for any property lacking a harness it can re-run to VERIFICATION SUCCESSFUL, a completed run lever-battery, or a resolvable delegation, it returns UNRESOLVED and exits non-zero — the hand-back fails. (An advisory miss_class: AGENT you leave behind is your own admission the item is unfinished, never a verdict.) There is no "partial run" hand-back and no asking the user to accept the remainder — you either finish (every property the scorer re-runs to proved / delegated to a named component / tool-boundary with a captured signature that survives the lever battery) or you keep working. The highest-leverage unfinished items are the shared/global invariants (Step 2, ordered by attachment count); the scorer flags them first because one left unattempted keeps every method in its bundle unproved.

Clean-slate re-run protocol (mandatory for re-runs)

A re-run must not inherit credit from a prior run's artifacts.

• Start from a stripped, isolated tree. New worktree; remove all existing #[cfg(kani)] mod verification harnesses so every one is re-authored from the inventory. You may not point at pre-existing harnesses to claim coverage.
• Do NOT delete the previous verified run. It stays on its committed verif/kani/<component> branch as the baseline and as evidence — deletion destroys expensive proofs and the ability to catch regressions.
• Provenance rule: a property counts as proved only if its harness was authored and is passing in this run's tree. A prior-run pass does not count until reproduced here.
• Diff against the baseline and report three sets: re-proved, regressed, and prior-"proved" that did not reproduce (phantom coverage). That diff is the audit.
• Capture wall-clock + peak RSS for every harness in the fresh run.

What each kani: block must record (per id)

Write these into unified_properties.yaml; there is no .md — the YAML is the record and the HTML (Role 3) is the human-readable form.

• Proved rows: status: proved, symbol: ✓ (native) or ★ (disclosed faithful stub/mirror), the fidelity (real-type-bounded / representative / arithmetic-core / bounded-shallow), and evidence with the harness name, Kani result, unwind: N, any flags (e.g. --no-unwinding-checks), wall-clock + peak RSS. State the bounded geometry in note — and for bounded-shallow, the loop-cut caveat (sound only when every loop runs ≤N) plus the Creusot route for a fully-sound proof.
• Assumptions / bounds: record each kani::assume(...) (the production guard it mirrors) and each stubbed FFI / #[kani::unwind(N)] bound — and what it leaves unproven — in the note of the property it affects.
• Not verified — attempted, tool boundary hit: status: tool-boundary, symbol: ⊘, miss_class: TOOL, and a note giving the geometry tried (unwind=K, structure size / stub used) and the concrete signature (unwinding-assertion at unwind=K / unsupported_construct: _xgetbv / SAT timeout >N min).
• Not verified — not expressible for a bounded checker: status: tool-boundary, symbol: ⊘, note with the one-line reason (concurrency/liveness, unbounded-only, or I/O/hardware/FFI) and the route (Creusot / Loom / Spin / fault-injection test). Note: string/char CONTENT is not in this bucket — it is expressible bounded (prove it); this bucket is for concurrency, unbounded-only, and I/O/hardware/FFI.
• Delegated: status: delegated, symbol: ⤴, note naming the owning component/test.

Notes

• Construction + documentation skill — distinct from the read-only audits component-check-spec-translation / component-check-verif-translation, from the source-agnostic extraction primitive extract-verifiable-properties, and from the inventory builder build-property-inventory (Role 1) whose output this skill consumes by id.
• Every outcome is written to unified_properties.yaml's kani: block by id, so tools-aggregate-coverage-by-interface (Role 3) renders from structured data without re-reconciling.
• Routing: Kani proof code (the #[cfg(kani)] mod verification harnesses + the unified_properties.yaml write-back) → the per-component verif/kani/<name> branch, overwrite-in-place, committed only under components/<name>/. Under the component-verify orchestrator, the orchestrator performs the branch/commit/push and enforces the component-folder-only contamination gate — this skill just leaves the artifacts in the working tree.