tools-verify-creusot-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 Creusot and record exactly what was proved. Inputs are the component's spec (the intended behavior) and its Rust code (the functions to prove). Outputs are (1) the Creusot verif/ artifacts and (2) the per-property status/symbol/ fidelity/evidence written back into the shared unified_properties.yaml under each property's creusot: block.

This skill = tools-verify-creusot + explicit spec pairing + a status-write-back step. Use tools-verify-creusot for the create/proof mechanics (pure-core extraction, verif/ crate, #[requires]/#[ensures], drift/equality check, fault-injection validation). This skill adds the spec-derived-contract sourcing and the structured write-back into unified_properties.yaml.

Steps

0. Environment — make the toolchain reachable FIRST (mandatory). The agent/tool shell does not source ~/.bashrc, so the bundled Creusot toolchain (why3 + the SMT provers) is off PATH by default. Before any cargo creusot, self-establish it and confirm the provers are registered — a "why3 not found" / "no prover" error is an environment fault to fix here, never a tool-boundary and never a reason to leave a property unattempted:

   export PATH="$HOME/.local/share/creusot/bin:$PATH"   # why3 + alt-ergo/cvc4/cvc5/z3 (absolute paths in ~/.why3.conf)
   command -v why3 >/dev/null || { echo "FATAL: why3 unreachable — creusot bundle missing, escalate to user"; exit 1; }
   why3 config detect >/dev/null 2>&1 || true           # re-register provers if ~/.why3.conf lost them
   why3 config list-provers | grep -qiE "alt-ergo|z3|cvc" || { echo "FATAL: no SMT prover registered"; exit 1; }
   

   Prepend the same PATH export to every heredoc/cargo creusot invocation in this run (a fresh tool shell starts without it). If the bundle itself is genuinely absent, that is a blocker to escalate to the user, not a per-property verdict — it does not license leaving any property unattempted.
1. Resolve inputs — consume the inventory, do NOT re-extract. Resolve to components/<name>/ and 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 to prove (src/**); use the spec only to read the wording of an obligation, 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 there — never keep a private property.
2. Prove the shared/global invariants FIRST, once — then reuse. Before any per-method work, take the inventory properties whose bundle spans multiple methods (the inventory marks these as global / maintained invariants and gives each an attachment count). Order them by attachment count, highest first — the one in the most bundles has the most leverage. Prove each as a single maintained invariant (a type #[invariant] or a logic predicate): establish it at construction/initialize, and prove each mutator preserves it (#[requires] inv(self) → #[ensures] inv(result)). Record it under its one inventory id — its proved status then propagates to every bundle it belongs to automatically (Role 3 attaches by id; you do NOT re-prove it per method). A cheap invariant in many bundles (e.g. an init-gate or an accounting invariant) unblocks all those methods in one proof — never skip it because "no single method owns it," and never re-assert it vacuously in each method.
3. Then, for each remaining per-method obligation, express it as a Creusot contract bound to the CODE. Take the obligation verbatim from its inventory row (id, statement, kind, object_fn) and render it as #[requires]/#[ensures] on the real function, citing the already-proved invariants as known facts rather than re-proving them. Where the crate can't build under Creusot, use a faithful whole-function mirror in verif/ with the same contract, guarded by a drift/equality check. Function granularity — never a lifted statement.
4. Prove. cargo creusot to green; iterate. Record every #[trusted] boundary and assumption.
5. Validate (anti-vacuity). Fault-inject each function (a contract-violating change) and confirm the proof goes red; if it stays green, the contract is vacuous — strengthen it. Then revert. For a maintained invariant, also fault-inject a mutator that breaks it and confirm the preservation VC fails.
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 re-runs cargo creusot from source (it touches every src/**.rs first, so a hand-edited .coma cannot fake a Proved). Your job in Step 6 is to leave, for every property, a proof unit the scorer can name and run:
   • One why3 module per property id — a function or lemma named verify_<id> (id lowercased, -→_) carrying the contract, so it compiles to verif/<crate>_rlib/verify_<id>.coma. If the obligation is discharged inside a differently-named module, point the scorer at it with creusot.evidence.module: <name> (or modules: [<a>, <b>] when several must all prove) — but each named module must exist and prove.
   • For any property you cannot prove on the first clean attempt, build the lever-battery variants that gate/lever_battery_creusot.yaml requires for the failure class you hit, as named modules: verify_<id>__inv (strengthened invariant), lemma_<id> (inductive #[logic] lemma), verify_<id>__fmap (FMap/Seq ghost mirror of a std container), verify_<id>__trusted (opaque type behind a contract-carrying #[trusted] u64-handle boundary). The scorer runs the scorer-applied levers itself (prover portfolio -P alt-ergo,z3,cvc5,cvc4, --time/--depth budget, -T split_vc,compute_specified); the code levers above it demands as artifacts. A tool-boundary is inadmissible until every required code-lever module exists — a missing one scores UNRESOLVED, not tool-boundary.
   • An anti-vacuity twin verify_<id>__mutant (a contract-violating copy) wherever the property could pass vacuously — the scorer requires it to go RED.
   • In unified_properties.yaml under the creusot: block you may fill only the advisory fields the scorer does not own: fidelity (real-type | ghost-mirror | trusted-boundary), a human note (name every #[trusted] boundary and what it therefore does not prove), the evidence.module(s) pointer above, and for a genuine cross-component delegation a resolvable delegate_to:. Do NOT write status, symbol, or the run-measured evidence (vcs/coma/wall/rss) — the scorer overwrites them from the live run and stamps _scored_by: scorer_creusot. The only way to move a property's status is to make its module reproduce. fidelity meanings: real-type = proved against the real product code; ghost-mirror = proved against a logic FMap/Seq model of the real container (★); trusted-boundary = the effect sits behind a contract-carrying #[trusted] boundary (block-device I/O, crc32fast, UTF-16, Mutex, raw ptr/FFI) (★). Report evidence in prose as VCs/goals discharged + .coma count — never bare "files".
7. Gate — the shipped scorer decides, by reproduction (mandatory; you cannot grade yourself). The reproduction gate is scorer_creusot.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_creusot.py" \
       components/<name>/verif --crate-dir components/<name>/verif --cap-seconds <cap>
   

   The scorer touches all sources (anti-tamper), runs scoped cargo creusot <module> for each property's module(s) (a Proved (…) ✔ with no ✘/unproved and exit 0 is a pass), captures VCs/.coma/wall/RSS from the run, checks the anti-vacuity mutant, applies the scorer-owned levers on failure, and writes the scorer-owned status/evidence/note/_scored_by. It assigns proved / tool-boundary (only after the scorer-applied levers ran, every required code-lever module was present and re-run, and the residual signature is not a known defeat) / delegated (resolvable referent) / UNRESOLVED (no module, an unreproducible pass, a missing required code-lever module, a known-defeat signature, or a broken/untranslatable crate) — 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 module / the demanded lever module / fix the crate, and re-run the scorer. Iterate until it exits 0. A translate error in the real verif crate is a broken crate (UNRESOLVED), never a tool-boundary. "Better suited to Kani" is not an exit — a within-component obligation Creusot genuinely cannot express earns a tool-boundary only by mapping to an active construct in gate/inexpressible_creusot.yaml (add claims_inexpressible: <IX-ID>; the scorer confirms it via an isolated canonical probe and records the covering tool from the entry's covered_by). It is not a delegation (delegation crosses a component boundary). You may not hand back the run or write a "partial run" summary while the scorer fails, no matter how many properties are proved; editing the YAML to say proved does nothing, since the scorer regenerates from source and overwrites it.

Coverage discipline (mandatory)

Attempt every property in the inventory that you can express as a contract. You do not get to pick lanes here — routing properties across tools is a separate step, not this one. Your job is to prove 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 Kani", "intractable", "needs induction", "to stay within budget" are not acceptable reasons to omit a property. If you can state the contract, you must attempt the proof.
• Attack the highest-leverage properties first. A property in many bundles is not lower priority for being "shared infrastructure" — it is higher priority, because one proof discharges it everywhere. Prove the shared/global invariants (ordered by attachment count) before spending effort on method-specific obligations; a cheap invariant left at not_yet silently keeps every method in its bundle unproved.
• Exhaust Creusot's capabilities before declaring a limit. Bit-level properties → #[bitwise_proof] (reasons over &/|/<</>> and Vec<u64> words — a bitmap round-trip is in scope, prove it). Maps/collections → logic-level FMap/Seq models. Nonlinear/division facts → proof_assert! bridges. Do not defer a bit-vector or container obligation as "out of reach" without first trying these.
• Bounded effort, not infinite grind. Give each proof a real attempt against a stated cap (e.g. one full portfolio pass, or a per-VC solver timeout). Exceeding the cap converts the property to a tool-boundary with the solver-timeout signature (miss_class: TOOL, note: the exact >N min, portfolio alt-ergo/z3/cvc5 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: the failing VC, a solver timeout (>N min, portfolio alt-ergo/z3/cvc5), or a specific SMT model gap (e.g. leading_zeros modelled only relationally, so leading_zeros ↔ log2 won't discharge). 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 in Creusot's logic at all — and inexpressibility is not yours to assert from a hunch: it holds only when the property maps to an active construct in gate/inexpressible_creusot.yaml (a documented tool-model fact), which you claim with claims_inexpressible: <IX-ID> for the scorer to confirm (see the record-format section). Concurrency/interleaving and liveness/timing are delegated to a concurrency model (Loom/Spin), not claimed here; (b) Depends on effects Creusot cannot model — real I/O, hardware, FFI byte layout. Everything else must be attempted and reported with its signature under the tool-boundary shape.

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. In particular a HashMap/HashSet-backed field is not an automatic boundary: creusot-std already gives it a View (ViewTy = FMap<K::DeepModelTy, V>) and you supply the mutation specs yourself.

• HashMap / HashSet field (insert/get/remove/contains/len). DEFEATABLE. The @ model exists but creusot-std ships specs for iteration only — write your own extern_spec! against the FMap API to give the mutators semantics:

  use creusot_std::{logic::FMap, prelude::*};
  use std::collections::HashMap; use std::hash::{BuildHasher, Hash};
  extern_spec! {
      impl<K: DeepModel + Eq + Hash, V, S: BuildHasher> HashMap<K, V, S> {
          #[check(ghost)]
          #[ensures((^self)@ == (*self)@.insert(key.deep_model(), value))]
          #[ensures(result == (*self)@.get(key.deep_model()))]
          fn insert(&mut self, key: K, value: V) -> Option<V>;
          // ...get / remove: see catalog §5 for the full Borrow/DeepModel-bounded block
      }
  }
  

  Fidelity ghost-mirror (symbol ★): you assert DeepModel equality coincides with Eq/Hash. Ship this extern_spec! block once as shared project infrastructure, not per-component.
• extern "C" / raw-pointer / FFI in the path. #[trusted] program fn with the real unsafe body + a contract that models the C effect logically + a ghost Ghost<Perm<*const T>> permission token the caller threads through (creusot-std/src/std/ptr.rs:555-660). Fidelity trusted-boundary (★). Only ⊘ if no faithful effect model exists.
• Foreign/std fn with no spec. extern_spec! { impl … { #[ensures(...)] fn … ; } } attaches a contract to a fn you don't own (the Vec→Seq pattern). #[trusted] for a whole opaque body.
• Trusted modules to widen coverage (contract-carrying #[trusted] boundaries — the coverage-over-a-hard-leaf lever). When a leaf fn/module is genuinely hard for Creusot (Creusot can't build it, a solver times out on its body, or it wraps an effect Creusot can't model), do not let it sink the whole call graph. Mark that leaf #[trusted] and give it a full #[ensures]/#[requires] contract stating what it guarantees; the callers above it then verify natively against that contract instead of inlining the unprovable body. One trusted leaf with a good contract can unblock many callers — this is the primary lever for raising the percentage of code Creusot covers. Discipline that keeps it honest, not a rug:
  • A #[trusted] contract is a promise, not a proof. It is an obligation you have shifted, not discharged. Every trusted item must be recorded per-property as fidelity: trusted-boundary (★), with the note naming why it is trusted and what it therefore does not prove. Never mark a leaf trusted merely because proving it is tedious — only when a lever above genuinely failed (capture that signature).
  • Make the contract as tight as the real behavior — an over-strong trusted #[ensures] silently makes every caller's proof vacuous. Anti-vacuity still applies: fault-inject a caller to confirm the caller proof depends on the trusted contract (goes red), and where feasible discharge the trusted contract by other means (a Kani harness over the leaf, a runtime witness test, or a later native Creusot proof) and cite that route in the note. Untrusted-by-another-tool > trusted-and-unchecked.
  • Keep the trusted surface small and explicit. Prefer trusting one narrow leaf over a broad module; the coverage you claim is "callers proved given these N trusted contracts", and Role 3 must be able to list those N. Shrink the trusted set over time as real proofs replace the promises.
• Complex / unbounded body. Decompose via sub-fn contracts + loop #[invariant]/#[variant] (termination measure) + #[maintains(inv)] to thread the data-structure invariant; call sites use only the contract.
• Bit-level property. #[bitwise_proof] reasons over &/|/<</>> and Vec<u64> words — a bitmap round-trip is in scope.
• Reference: verif/skills_research/CREUSOT_capability_catalog.md in the eviction-policy-session-lists component carries the full catalog (0.12 renames, extern_spec! HashMap→FMap recipe with copy-paste get/remove, the Ghost<Perm> FFI pattern, soundness costs).

Crate hygiene and proof engineering — measured, not theoretical (mandatory)

🔴 NEVER put [patch.crates-io] in components/<component>/.cargo/config.toml

Put the creusot-std patch in verif-creusot/Cargo.toml, as a manifest-level patch, with a checkout-relative path (creusot-std = { path = "../creusot/creusot-std" } via the gitignored components/<component>/creusot symlink).

A cargo config at component scope applies to EVERY cargo invocation whose cwd is anywhere inside the component — including cargo kani and the Kani scorer's cargo metadata preflight, which then die in dependency resolution on a crate they have no reason to load. This has now happened TWICE (block-device-filesys, then eviction-policy-session-lists). The second time it would have aborted the entire Kani gate before it scored a single property; it was caught only because the Kani agent reported it. A manifest-level [patch] is scoped to the one crate and is always the right home. Note cargo metadata --no-deps does NOT reveal this fault (measured: it returns 0 while full resolution fails), which is why the Kani doctor deliberately omits that flag.

Splitting a multi-conjunct invariant is NECESSARY BUT NOT SUFFICIENT

split_vc splits goal structure, not a predicate body. So N conjuncts hidden behind a single #[ensures(pool_inv(&^p))] collapse into ONE goal and fail, while each conjunct closes on its own. Therefore: give each mutator one #[ensures] per clause, and define every composite predicate as the conjunction of its named halves, so re-deriving the composite is a definitional unfolding. Measured: this took pool_touch from failing to proved, and pool_register from 3 open goals to 2.

But separating them does not, by itself, close them — and the reason is NOT what an earlier version of this section claimed. It said the residue was budget starvation ("many goals in one why3 file degrade the harder ones"). That was never measured, and it is wrong. When pool_unlink's 22 remaining goals were finally closed, the causes were identified by decoding proof.json and were four missing facts plus three collateral positions — not starvation:

• the two levers the starvation theory recommends were both tried and both failed. Raising the budget (-t 90 -d 20 -j 16) on pool_unlink alone ran 35 minutes without finishing and had to be killed; the gate's cap is 120-600 s, so that route is disqualified on cost. Dropping the composite clauses would have removed only the 3 collateral positions (9 of 22) and left all 4 root causes untouched, at the price of making ~40 driver modules unfold the invariant themselves.
• what actually worked was shape, covered in the next section: positional provenance clauses on the four container primitives (19 goals), plus putting the model's one existential behind a named #[logic] predicate and supplying the witness term no prover invents (3 goals).

So when goals survive the split, decode which ones and why before reaching for a bigger budget. The recipe: the first split_vc under vc_<fn> yields exactly one child per #[ensures] in source order, so proof.json tells you precisely which clause fails. Distinguish a root cause from a composite that merely contains one. Chasing budget first cost 35 minutes for nothing.

One genuine budget caveat, separate from the above: a clause proving at 29.0 s against a 20 s budget passes only intermittently and will flip under load — which is why one helper read "2 open" rather than "1". If a goal's time is near the budget, treat it as failing.

State a preservation postcondition in the SAME SHAPE as the invariant that consumes it

A logically equivalent phrasing is not an equivalent hypothesis, and this is the lever that actually closes invariant-preservation goals. The rule, measured:

• an invariant that quantifies over a POSITION needs a positional preservation clause;
• one that quantifies over a VALUE needs a membership clause;
• a container primitive is used by both, so it needs both;
• any exists belongs behind a named #[logic] predicate, with a wrapper that supplies the witness term explicitly — a prover will not invent it.

Measured on eviction-policy-session-lists: the existing clauses were all membership-shaped (map_has_i/leaves_mem_i), which is right for leaf_in_set and useless to idx_ok, by_key_entries_live and session_entries_ok, which quantify over a position — so the solver had to invent the position first. map_insert had no whole-range clause at all. Adding positional provenance to map_insert/map_remove/leaves_insert/leaves_remove took pool_unlink 22 → 8; putting the one existential behind free_covers with a free_push wrapper supplying free@.len() closed the rest and took all three helpers to 0 open. Side effect worth noting: one driver's proof went from 61 recorded prover calls to 8 — the right shape is also far cheaper.

The same principle unblocked three stale-handle refutations, which needed frame facts (slot reuse, key-index frame) rather than stronger ones.

cargo check is necessary but NOT sufficient

It does not reproduce pearlite-side errors: Int as u32, Clone ambiguous against the prelude glob, old() in a loop invariant, or recursion_limit = 1024 overflowing at ~31 #[ensures]. Only cargo creusot does. A verif crate that compiles can still be a broken verif crate, so "it builds" is never evidence. Still run cargo check — it caught two real Rust errors here (use of moved value, cannot move out of index). Derive-ambiguity fix: fully-qualified paths (#[derive(::core::clone::Clone, ::core::marker::Copy)]) and drop PartialEq/Eq, since deriving PartialEq additionally demands DeepModel while pearlite == is logical equality.

Driver goals that are NOT in the #[ensures] block — check here before blaming the helper

A driver whose own verify_<id> module fails may not be failing on its postcondition at all. The top-level split children before the exit VC are the #[requires] obligations of the calls the driver makes. Measured on eviction-policy-session-lists: ~22 properties fail exactly there, on the arithmetic side conditions every state-layer operation requires and none re-establishes (reads < u32::MAX-15, clock + n < u64::MAX-615, nodes.len() < u32::MAX-15, log capacity). A driver chaining two operations therefore cannot discharge the second call's precondition.

The fix is contract exposure, not prover tuning: have each state-layer operation ensure how much it consumed ("the arena grew by at most one", "the clock advanced by at most n", "reads grew by at most one"), so a chained caller can carry the bound forward. Recognise this class by reading WHICH split child failed — a missing precondition looks nothing like an unproved postcondition, but both surface as "module failed".

Two measurement traps that produce WRONG NUMBERS you will be tempted to report

• proof.json is written incrementally. A mid-run read is unreliable — pool_register read 0 unproved mid-run and 2 when finished. Gate every census on the printed Proved ✔ / Goal … ✘ (x/y) line, never on a mid-run proof.json. (This trap cost a wrong number in a hand-off report on the very run that discovered it.)
• why3find REPLAYS CACHED RESULTS. After changing a source, delete the module directory or pass --why3find-arg=-f, or you are measuring the previous run.

Dead end — do not retry

proof_assert! is unusable inside macro_rules! mutator bodies ("Use of borrowed or uninitialized variable p"), with or without explicit &mut *p reborrows. Bridging facts must live on callee contracts.

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 green proof (native), or a disclosed faithful whole-function mirror / #[trusted] 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 contract, ran the proof, and captured a reproducible failure signature (failing VC / solver timeout >N min portfolio / specific SMT model gap). Evidence is mandatory; a limit asserted without a proof attempt, or before trying the lever that clears it (e.g. the extern_spec! FMap recipe for a HashMap field), is not a legitimate boundary — it is a recipe gap.

"Contract not written" / "authorable but not done" is NOT an end state. A property with no contract 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 proof unit 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_creusot.py, which touches every source and re-runs cargo creusot from scratch: for any property lacking a proof unit it can re-run to Proved, 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; reduce every contract to a bare signature (drop #[ensures], #[requires(true)]) / empty the verif/ mirror, so every contract is re-authored from the inventory. You may not point at pre-existing contracts to claim coverage.
• Do NOT delete the previous verified run. It stays on its committed verif/creusot/<component> branch as the baseline and as evidence — deletion destroys expensive proofs (.coma/VCs) and the ability to catch regressions.
• Provenance rule: a property counts as proved only if its contract was authored and its VCs are discharged 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 proof in the fresh run; report proofs as VCs/goals discharged + .coma count, never bare "files".

What each creusot: 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 ★ (faithful ghost mirror / #[trusted] boundary), the fidelity, and evidence as VCs/goals discharged + .coma count (never "files") with wall-clock + peak RSS. If the proof is against a mirror, say what it therefore does not cover in note.
• Trusted boundaries: name each #[trusted] item / mirror / environment assumption in the note of the property it guards — why trusted, and what it therefore does NOT prove (fidelity: trusted-boundary, ★).
• Not proved — attempted, tool boundary hit: status: tool-boundary, symbol: ⊘, miss_class: TOOL, and a note giving the capability tried (#[bitwise_proof] / FMap / proof_assert!) and the concrete signature that blocked it (failing VC / solver timeout >N min / SMT model gap).
• Not proved — genuinely NOT EXPRESSIBLE in Creusot: you do not write status or a prose excuse. A property is inexpressible only if it maps to an active construct in gate/inexpressible_creusot.yaml — a curated, documented tool-model fact (e.g. IX-CREUSOT-STRING-CONTENT: concrete string/char CONTENT sits behind an opaque Seq<char> view). If it does, add claims_inexpressible: <IX-ID> to the property's creusot: block (an advisory claim, not a verdict) and stop — the scorer confirms it by building that construct's canonical probe in isolation and observing the model-predicted signature; only then does it award tool-boundary (fidelity: not-expressible, covered_by recorded). You may only reference an existing active construct — never invent one, and never use this for "hard to prove." A goal you can state but the solver won't discharge is bucket (a) above (battery + captured signature), not this. If no construct fits, the property is either provable (attempt it) or a concurrency/interleaving obligation that is delegated to Loom/Spin (a different model), not an inexpressibility claim here.
• 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 creusot: block by id, so tools-aggregate-coverage-by-interface (Role 3) renders from structured data without re-reconciling.
• Routing: Creusot proof code (the verif/ crate + .coma + the unified_properties.yaml write-back) → the per-component verif/creusot/<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.