When to reach for the new skills

The recent catalogue extensions cover state-machine modelling, verification, supply chain, decision records, and Polonius migration. The short versions follow.

Use this skill for parsers, codecs, protocols, actors, device lifecycles, or any state carrier built from correlated booleans, Option fields, sentinel values, or fields that must change together. It distinguishes caller-driven finite operation sequences, where typestate may prevent real misuse, from input- or event-driven machines, where a stable owner with a runtime ADT is normally the right representation. Its references cover parser, protocol, asynchronous, and device patterns plus transition-table, trybuild, property, Kani, and concurrency testing.

A device lifecycle shows both layers in one machine: configuration is caller-driven, while the transfer phases inside Enabled are driven by device events.

For screen readers: The following state diagram shows a device lifecycle that is configured by its caller, then driven by transfer and fault events once enabled.

Figure 2: Device lifecycle — caller-driven configuration wrapping an event-driven transfer state machine.

The decisive question is who chooses the next transition. A caller-selected finite sequence can be enforced by typestate; input, frames, socket readiness, or interrupts cannot, and belong in a runtime ADT behind one stable owner.

For screen readers: The following flowchart shows how to choose between typestate and a runtime algebraic data type (ADT) based on who selects the next transition.

Figure 3: Selecting a state representation by transition ownership.

Use this skill to assess Polonius adoption, audit suspected NLL workarounds, or improve ownership and borrow-centric APIs. Treat ownership/API improvements as independent of compiler adoption: establish checker-dependent gains by comparing the proposed replacement with explicit -Zpolonius=off and -Zpolonius=next on one pinned compiler, and decide compiler-support policy separately. See the verification protocol for reproducible controls and attribution rules. It distinguishes borrow limitations Polonius may remove from aliasing, async, and thread-boundary constraints that still require ownership. Routine borrow errors continue to route to rust-memory-and-state.

Use this skill when you need to prove or disprove a property and are unsure whether to reach for Miri, sanitizers, property tests, cargo-mutants, loom, shuttle, turmoil, Kani, or Verus. The skill's selection table maps failure modes to tools. From there it routes into the proptest, kani, and verus deep dives.

Use this skill when a pure function has a property (round-trip, idempotence, ordering, conservation) that is easier to state than to enumerate, or when a parser or codec must round-trip across all valid inputs. The skill covers strategy design with prop_compose!, the filtering trap and its fix, regression-file discipline, state-machine tests via proptest-state-machine, and the proptest-derive vs test-strategy choice. It also answers the question reviewers ask first, whether a change needs a property test at all, and ships a review checklist and a sibling-module template drawn from the estate's review history.

Use this skill when ordinary Rust unit tests need clearer structure: rstest fixtures and parameterized cases, fallible setup helpers, serial_test for genuine global-state isolation, rich matcher assertions with googletest, diff-friendly equality with pretty_assertions, and snapshot tests with insta. It also carries a worked example for splitting one mixed assertion helper into extraction, pure comparison, and a thin assertion wrapper.

Use this skill when writing a harness for a small, well-bounded property: an arithmetic invariant, a parser corner case, or a state machine with a small alphabet. Kani is unwind-bounded by default; the skill describes how to set #[kani::unwind(n)], when to use kani::any and kani::assume, and when to escalate to Verus instead. Its references carry the project on-ramp (pins, Makefile targets that delegate to prover-tools, smoke and nightly CI, contract tests) and the review checklist for vacuous harnesses, model drift, solver cliffs, and the cfg(kani) build.

Use this skill when the property must hold for unbounded inputs, when the bounded loop in Kani times out, or when the proof composes several lemmas. The skill covers spec/proof/exec mode discipline, trigger heuristics for the underlying Z3 solver, the broadcast use pattern for sequence axioms, and the layout of a proof project that mirrors a production module, including the refinement lemma that binds an idealized spec to the runtime structure. Its references carry the on-ramp and review checklist.

The survey these checklists come from is docs/verification-review-failure-modes.md.

Use this skill when adding a dependency, tightening a lockfile policy, configuring cargo-vet or cargo-deny, or wiring SemVer guardrails (cargo-semver-checks, cargo-public-api) into release. The references describe a decentralized audit setup with imports from the Bytecode Alliance and Mozilla, plus a deny.toml policy template.

Use this skill when capturing a decision that is hard to reverse — a typestate, an unsafe invariant, a verification-tool choice, a public API shape. The skill gives the six-clause Y-Statement template and three worked Rust examples, and explains how to supersede an earlier ADR cleanly.