asterinas
- 12 skills
- 0 followers
- 16 hours ago last updated
- ▌ Aster Code Review · asterinas bundleReview code against Asterinas's persona-keyed coding guidelines and write a Markdown review file. Use when asked to review a Git change (diff mode) or a set of target files (files mode) for defects, or inside a write-test-review loop.
- ▌ Kverus Fix · asterinas bundleFix Verus verification errors by iterating minimal proof-preserving edits until verification succeeds. Use with an explicit target and verification command, or automatically discover the command and locate the target from fresh diagnostics when either input is unavailable.
- ▌ Kverus Run · asterinas bundleRun the full Rust-to-Verus pipeline (migrate → spec → fix → eval → semantic audit → postprocess) in one command. Use when converting Rust code to verified Verus code end-to-end.
- ▌ Kverus Eval · asterinas bundleEvaluate current unstaged spec modifications for semantic quality and intent preservation, then score the modification out of 10. Use when reviewing spec edits before staging or committing.
- ▌ Kverus Spec · asterinas bundleAdd Verus specification scaffolding to an entry target file while preserving executable behavior. Use when you want stronger proof-ready specs (requires, ensures, invariants, decreases, recommends, spec helpers) without fully finishing proofs.
- ▌ Kverus Strip · asterinas bundleAggressively strip redundant proof code from a Verus codebase while keeping verification passing. Use when you want to slim down Verus proof bloat, simplify redundant proof asserts, or run postprocess cleanup without breaking verification.
- ▌ Kverus Common · asterinas bundleShared Rust/Verus proof references for other KVerus skills. Use when Codex is repairing Verus failures, adding specifications, migrating Rust, classifying axioms or trusted boundaries, modeling external APIs, or cleaning proof scaffolding.
- ▌ Kverus Review · asterinas bundleReview uncommitted or recent Verus code changes for exec-code modifications, unnecessary =~= introductions, and verification issues. Use before committing to catch regressions in executable semantics, set reasoning, and proof quality.
- ▌ Kverus Migrate · asterinas bundleConvert a Rust target into minimally modified Verus-compatible code using an explicit verification command. Use when migrating a specific file and iterating until the verification command succeeds.
- ▌ Kverus Common Sync · asterinas bundleCheck whether the installed `kverus-common` skill stays synchronized with the local Verus guide under `database/verified/code/tools/verus/source/docs/guide/src`. Use when validating kverus-common after guide updates, before committing skill changes, or when checking for stale guide-derived references and missing source files.
- ▌ Kverus Postprocess · asterinas bundleFinal cleanup for Verus proof changes: consume cached dynamic review rules, delegate stale GitHub refreshes to a subagent, verify, simplify redundant proof code through kverus-strip, format, and run local checks. Use after proof-sensitive KVerus work or before finalizing Verus changes.
- ▌ Kverus Semantic Audit · asterinas bundleCompare original Rust source folders against migrated Verus code folders, identify executable-code differences that may change runtime semantics, and write per-file audit reports to an output folder. Use when checking whether Rust-to-Verus rewriting preserved executable behavior rather than merely verifying successfully.