What is kverus-postprocess?

A cleanup workflow for Verus proof changes. Verus is a Rust-based tool for formally checking that code meets stated rules.

Use it after changing Verus specifications or before finalizing them, with a base revision, target paths, verification command, and formatter command.

It helps remove unnecessary proof code, apply review rules, format the files, and check that the changes still pass verification.

kverus-postprocess — Skill for Codex by asterinas/KVerus

Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

Any agent

npx skills add asterinas/KVerus --skill kverus-postprocess

Clone the repo

git clone --depth 1 https://github.com/asterinas/KVerus

Made for: Codex.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

README.md

[![agentmods](https://agentmods.dev/badge/skills/asterinas/kverus/kverus-postprocess/github.svg)](https://agentmods.dev/skills/asterinas/kverus/kverus-postprocess)

Your own site

<a href="https://agentmods.dev/skills/asterinas/kverus/kverus-postprocess"><img src="https://agentmods.dev/badge/skills/asterinas/kverus/kverus-postprocess/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

Your own site · 80×15

<a href="https://agentmods.dev/skills/asterinas/kverus/kverus-postprocess"><img src="https://agentmods.dev/badge/skills/asterinas/kverus/kverus-postprocess.svg" alt="Reviewed on agentmods" width="80" height="20"></a>

Per session 66 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.

When invoked 1,392 The whole file, excluding the scripts and references it only reads on demand.

Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe. Third-party audits

NVIDIA SkillSpector pass 7 Sept 2026

How audits are shown

Origin original No closer match found in the catalogue.

Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

Model	Per session	Once invoked
Fable 5.1	$0.00066	$0.01392
Opus 5.5	$0.00026	$0.00557
Sonnet 5.5	$0.00013	$0.00278
Haiku 4.5	$0.00007	$0.00139

Measured 1mo ago against content hash f1b6cfcbc6a0, method: parsed. Prices are Anthropic first-party input rates as of 2026-10-07, from the pricing page.

Security

Grade A, and why

kverus-postprocess scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 1mo ago.

The scan reads SKILL.md. This mod also ships 3 executable files (scripts/kverus_postprocess.py, scripts/run_postprocess.ps1, scripts/run_postprocess.sh), listed below but not scanned — reading those needs a real analyzer, not pattern matching.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

skills/kverus-postprocess/SKILL.md · 125 lines

How it starts

The opening of the file, as written. The whole thing — 125 lines — stays where its author put it; the contents beside it link to each section on GitHub.

KVerus Postprocess

Set AGENT_DIR to the installed agent directory when running commands manually. Skills are read from $AGENT_DIR/skills.

Required Inputs

base: git base ref for diff context, e.g. origin/main.
target-path: changed source paths to inspect and simplify, e.g. src/,specs/.
verify-command: full verification command. If unavailable, simplification must run in --dry-run.
format-command: project formatter command, e.g. cargo fmt, make fmt, or an equivalent.
Optional rule-repo: GitHub owner/repo used for dynamic review rules.
Optional scope controls: blocked-path for path prefixes that must not change, and generated-path for generated artifact prefixes.

Workflow

Inspect the dynamic-rule cache without accessing GitHub:

. "$AGENT_DIR/kverus.env"
"$KVERUS_PYTHON" "$AGENT_DIR/skills/kverus-postprocess/scripts/kverus_postprocess.py" \
  --rule-repo <owner/repo> \
  --cache-status

The default cache TTL is 72 hours. If the cache is stale or missing and subagents are available, delegate exactly one bounded refresh task to a subagent:

. "$AGENT_DIR/kverus.env"
"$KVERUS_PYTHON" "$AGENT_DIR/skills/kverus-postprocess/scripts/kverus_postprocess.py" \
  --rule-repo <owner/repo> \
  --refresh-only

Tell the subagent to run only this command, preserve any old cache on failure, make no source edits, and return a concise status. Continue the main workflow immediately instead of waiting for GitHub. If subagents are unavailable, keep using the old cache or static rules; do not perform an automatic synchronous refresh in the main agent.

Run the local checker with --no-refresh-rules so it only consumes the latest available cache:

"$KVERUS_PYTHON" "$AGENT_DIR/skills/kverus-postprocess/scripts/kverus_postprocess.py" \
  --base <base-ref> \
  --target-path <path1,path2> \
  --rule-repo <owner/repo> \
  --no-refresh-rules

Fix every ERROR. Review every WARN and fix it unless there is a clear reason to keep the code.

Read the full file on GitHub · 125 lines

Files

What ships with it

6 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

1mo ago Changed · +24 lines f1b6cfcbc6a0
1mo ago First seen · 101 lines · 66 tokens per session scan A fea705e52745

Subscribe to this mod's changes

kverus-postprocess is a skill published in the GitHub repository asterinas/KVerus (27 stars, last pushed 10d ago), licensed MIT. It adds 66 tokens to every session and 1,392 once invoked, about $0.0003 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.

Building agents Code review LLM Rust formal-verification

github-code-review

Review code changes by analyzing git diffs, leaving inline comments on PRs, and performing thorough pre-push review. Works with gh CLI or falls back to git + GitHub REST API via curl.

moltis-org/moltis · 45 tokens

github

GitHub operations via gh CLI: issues, PRs, CI runs, code review, API queries. Use when: (1) checking PR status or CI, (2) creating/commenting on issues, (3) listing/filtering PRs or issues, (4) viewing run logs. NOT for: complex web UI interactions requiring manual browser flows (use browser tooling when available)…

moltis-org/moltis · 101 tokens

requesting-code-review

Pre-commit verification pipeline — static security scan, baseline-aware quality gates, independent reviewer subagent, and auto-fix loop. Use after code changes and before committing, pushing, or opening a PR.

moltis-org/moltis · 46 tokens

review

Review code changes, pull requests, patches, or a scoped code area for actionable correctness, security, compatibility, and test risks with file and line evidence. Use for review or audit requests; do not use for general proofreading, feature implementation, or debugging a reported failure when the user wants a fix.

bigduu/Bamboo-agent · 62 tokens

debug

Diagnose a concrete failure, regression, crash, hang, flaky test, or incorrect runtime behavior by reproducing it, testing hypotheses, and identifying the evidence-backed root cause. Use when symptoms or failing output exist; do not use for feature implementation without a failure, general code review, or a conceptual…

bigduu/Bamboo-agent · 64 tokens

simplify

Reduce unnecessary code complexity, duplication, indirection, or abstraction while preserving observable behavior and validating equivalence. Use for simplify, cleanup, or behavior-preserving refactor requests; do not use for adding features, diagnosing an unexplained failure, broad code review without a…

bigduu/Bamboo-agent · 68 tokens