| name | kverus-common |
| description | Shared Rust/Verus proof references and Asterinas/VOSTD project practices for other KVerus skills. Use when Codex is repairing Verus failures, adding specifications, migrating Rust, classifying axioms or trusted boundaries, modeling external APIs, cleaning proof scaffolding, or working with Asterinas/VOSTD verification conventions. |
KVerus Common
Use this skill as a shared reference layer for KVerus tasks. It does not define a standalone repair workflow; pair it with task skills such as kverus-fix, kverus-spec, or kverus-migrate.
Loading Rule
Before editing Verus code, load only the relevant reference:
- Syntax or mode confusion: read
references/verus-syntax-quickref.md.
- Verification repair strategy or error triage: read
references/common-errors.md.
- Proof construction, quantifiers, arithmetic, bit-vector, or SMT context issues: read the relevant file under
references/ — proof-localization.md, quantifiers.md, solvers.md, arithmetic-lemmas.md, calc-blocks.md, opaque-reveal.md, lemma-shape.md, or set-reasoning.md.
- Loop or recursive proof failures: read
references/invariants.md.
ghost, tracked, Tracked<T>, Ghost<T>, @, or erasure issues: read references/ghost-tracked.md.- Axiom-like declarations, external API specifications, trusted boundaries, or proof cleanup: read
references/proof-engineering-and-trust-boundaries.md.
- Missing or incomplete vstd specifications for , , or APIs: read together with .
