How do I install the Rust Verification skill?

Run npx skillmds@latest add tomevault-io/rust-verification in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Rust Verification safe to use?

This skill has not completed SkillMD's automated safety review yet. Independent scanners report: SkillSpector: PASS, Skill Scanner: PASS. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Rust Verification?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Rust Verification free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Rust Verification?

tomevault-io (@tomevault-io) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Rust Verification by tomevault-io — Agent Skill

Name: Rust Verification
Author: tomevault-io

Rust Verification

Select and combine Rust verification tools — Miri, sanitizers, property testing, mutation testing, deterministic concurrency exploration (loom, shuttle, turmoil), bounded model checking (Kani), and deductive proofs (Verus). Use when choosing the smallest tool that gives the required guarantee for a given failure mode. Use when this capability is needed.

tomevault-io Updated Sep 17, 2026

File contents

Rust verification: choosing the right adversary

Tests show a program works on the inputs you tried. Verification tools attack the program with adversaries chosen by failure mode: UB, unexpected inputs, schedule chaos, logic gaps, exhaustive state, or unbounded reasoning. Pick the smallest adversary that fits the property at risk.

Working stance

Name the failure mode before naming the tool.
Each tool is additive: Miri does not replace proptest, Kani does not replace Verus.
Run cheap adversaries on every change; reserve expensive sweeps for code where they pay back.
The effort is not finished until a deliberate mutation of the production code is caught by it.

Selection by failure mode

Failure mode	First reach
Undefined behaviour in `unsafe` (aliasing, init, UB)	Miri + sanitizers
Input gaps in pure functions	`proptest`
"My tests pass but my logic is wrong"	`cargo-mutants`
Async cancellation, ordering, partial-failure	`turmoil`
Atomic / lock-free memory ordering on a single core	`loom`
Mutex / channel scheduling on a single core	`shuttle`
Structural invariant over a bounded state space	`kani`
Algebraic property over an unbounded domain	`verus`

See references/tool-selection.md for a longer walkthrough with one paragraph per tool.

Layering rule

Climb only when the layer below is clean; bugs found higher up are much harder to diagnose.

Unit tests anchor concrete expectations.
Miri and sanitizers catch UB on the inputs tests already exercise.
proptest widens inputs; cargo-mutants checks the tests can fail.
loom, shuttle, and turmoil shake the schedule.
kani proves bounded structural invariants.
verus proves unbounded algebraic properties.

Deterministic chaos

loom, shuttle, turmoil, and kani require the system under test to be deterministic given its inputs. Hidden non-determinism (clocks, RNG, thread IDs, env reads) breaks reproduction. See references/deterministic-chaos.md for the fences chaos tools require.

Red flags

"We already test this" and a one-line mutation does not break the test.
An unsafe block has a safety comment but never runs under Miri.
A proptest regression file is checked in but never minimised or promoted to a unit test.
A Kani harness or Verus proof references symbols that no longer match production — the mirror is decaying.
Concurrency tests pass locally and flake in CI; loom, shuttle, or turmoil have not been tried.

Routing into deep dives

Strategy design, shrinking discipline, regression files, the filtering trap, and state-machine tests: proptest.
Kani harness shape, unwind discipline, contracts, stubbing: kani.
Verus modes, triggers, sequence proofs, assert by: verus.

Proptest is a regular Cargo dev-dependency; kani and verus install via rust-prover-tools. The selection rules above stay authoritative for picking between them.

References

references/tool-selection.md — per-tool "use when" rationale.
references/deterministic-chaos.md — determinism fences for chaos tools.
Deep dives: ../proptest/SKILL.md, ../kani/SKILL.md, ../verus/SKILL.md.

Source: leynos/rust-skill — distributed by TomeVault.

---name: rust-verificationdescription: Select and combine Rust verification tools — Miri, sanitizers, property testing, mutation testing, deterministic concurrency exploration (loom, shuttle, turmoil), bounded model checking (Kani), and deductive proofs (Verus). Use when choosing the smallest tool that gives the required guarantee for a given failure mode. Use when this capability is needed.---# Rust verification: choosing the right adversaryTests show a program works on the inputs you tried. Verification toolsattack the program with adversaries chosen by failure mode: UB,unexpected inputs, schedule chaos, logic gaps, exhaustive state, orunbounded reasoning. Pick the smallest adversary that fits the propertyat risk.## Working stance- Name the failure mode before naming the tool.- Each tool is additive: Miri does not replace proptest, Kani does not replace Verus.- Run cheap adversaries on every change; reserve expensive sweeps for code where they pay back.- The effort is not finished until a deliberate mutation of the production code is caught by it.## Selection by failure mode| Failure mode | First reach || ----------------------------------------------------- | ------------------ || Undefined behaviour in `unsafe` (aliasing, init, UB) | Miri + sanitizers || Input gaps in pure functions | `proptest` || "My tests pass but my logic is wrong" | `cargo-mutants` || Async cancellation, ordering, partial-failure | `turmoil` || Atomic / lock-free memory ordering on a single core | `loom` || Mutex / channel scheduling on a single core | `shuttle` || Structural invariant over a bounded state space | `kani` || Algebraic property over an unbounded domain | `verus` |See [`references/tool-selection.md`](references/tool-selection.md) for alonger walkthrough with one paragraph per tool.## Layering ruleClimb only when the layer below is clean; bugs found higher up are muchharder to diagnose.1. Unit tests anchor concrete expectations.2. Miri and sanitizers catch UB on the inputs tests already exercise.3. `proptest` widens inputs; `cargo-mutants` checks the tests can fail.4. `loom`, `shuttle`, and `turmoil` shake the schedule.5. `kani` proves bounded structural invariants.6. `verus` proves unbounded algebraic properties.## Deterministic chaos`loom`, `shuttle`, `turmoil`, and `kani` require the system under testto be deterministic given its inputs. Hidden non-determinism (clocks,RNG, thread IDs, env reads) breaks reproduction. See[`references/deterministic-chaos.md`](references/deterministic-chaos.md)for the fences chaos tools require.## Red flags- "We already test this" and a one-line mutation does not break the test.- An `unsafe` block has a safety comment but never runs under Miri.- A `proptest` regression file is checked in but never minimised or promoted to a unit test.- A Kani harness or Verus proof references symbols that no longer match production — the mirror is decaying.- Concurrency tests pass locally and flake in CI; `loom`, `shuttle`, or `turmoil` have not been tried.## Routing into deep dives- Strategy design, shrinking discipline, regression files, the filtering trap, and state-machine tests: [`proptest`](../proptest/SKILL.md).- Kani harness shape, unwind discipline, contracts, stubbing: [`kani`](../kani/SKILL.md).- Verus modes, triggers, sequence proofs, `assert by`: [`verus`](../verus/SKILL.md).Proptest is a regular Cargo dev-dependency; `kani` and `verus`install via[`rust-prover-tools`](https://github.com/leynos/rust-prover-tools).The selection rules above stay authoritative for picking betweenthem.## References- [`references/tool-selection.md`](references/tool-selection.md) — per-tool "use when" rationale.- [`references/deterministic-chaos.md`](references/deterministic-chaos.md) — determinism fences for chaos tools.- Deep dives: [`../proptest/SKILL.md`](../proptest/SKILL.md), [`../kani/SKILL.md`](../kani/SKILL.md), [`../verus/SKILL.md`](../verus/SKILL.md).---> Source: [leynos/rust-skill](https://github.com/leynos/rust-skill) — distributed by [TomeVault](https://tomevault.io).

Frequently asked questions