kverus-strip

Aggressively strip redundant proof code from a Verus codebase while keeping verification passing. Be as aggressive as possible — many proof blocks and assertions exist purely for human readability and are not needed for the SMT solver to succeed.

Preferred invocation:

$kverus-strip verify="<verification command>" target-dirs="<dir1,dir2>"

If verify is missing, ask for it before editing. If target-dirs is missing, first run the proof simplification script for changed files; ask for target-dirs only before doing broader manual proof-code stripping.

Arguments

• verify (required): The full verification command, e.g. cargo verus focus my_crate.
• target-dirs (required for broader manual stripping): Comma-separated source directories or single .rs files to scan, e.g. src/,specs/ or src/model/owners.rs. A path the script would otherwise need to discover can be passed directly here.
• function (optional): Comma-separated function short names to restrict stripping to, e.g. lemma_index_bounds. Only matching functions are processed; all others in the file are left untouched.
• base (optional): Git base ref for changed-file discovery, e.g. origin/main.

Shared Verus References

If understanding Verus proof constructs (proof blocks, ghost/tracked values, spec/proof functions) is needed before deciding deletions, read the relevant reference under ../kverus-common/references/ before editing.

Proof Simplification Script

For routine redundant proof-statement cleanup, prefer the bundled script before manual stripping:

. "$AGENT_DIR/kverus.env"
"$KVERUS_PYTHON" "$AGENT_DIR/skills/kverus-strip/scripts/simplify_proof.py" \
  --base <git-base> \
  --target-dir '<dir1,dir2>' \
  --verify-command '<verification command>' \
  --format-command '<format command>'

The script scans changed .rs files when no --target-dir or --file is provided. It simplifies at function scope, matches the src/refiner/simplifier.py policy, skips runtime assert!(...), never removes assert(false), skips functions containing admit, assume, or #[verifier::external_body] unless --deep-clean is set, removes one proof statement at a time, and keeps the removal only when the verification command still succeeds. With tree-sitter-verus, candidates include standalone function-call statements in proof fn, proof {}, and assertion proof blocks; executable calls are extracted but never offered for deletion. The default mode requires tree-sitter-verus and errors out if it is missing; pass --text-only to force the lower-precision text-based (asserts-only) parser. Use --dry-run to list candidates without editing.