KVerus Skills

KVerus is a skill-based workflow for migrating Rust code to Verus, adding proof-oriented specifications, repairing verification failures, and auditing the result. It can be used stage by stage through individual skills or end to end with kverus-run, which combines migration, specification, fixing, evaluation, semantic audit, and postprocessing into one verification pipeline.

The workflow-based version presented in the ASE '26 paper KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code is available on the ase-26 branch.

Setup Environment

0. Clone the Repo

$ git clone --recursive https://github.com/asterinas/KVerus.git

1. Prepare the python environment

If you don't have uv installed, please follow the official instructions.

# sync python environment
uv sync

[!NOTE] The Python environment is optional. kverus-strip uses treesitter-verus to parse Verus code more precisely, but it can also fall back to an LLM-based path without it. If you do not use an accurate kverus-strip, you can skip this step.

2. Install Verus

KVerus depends on the Verus command-line tool. See the official installation guide.

Setup Skills

KVerus ships a set of agent skills (under skills/) that can be installed into any target project for use with Codex or Claude Code.

# Install all skills into a target project (symlink mode, agent target by default)
$ ./scripts/install-skills.sh ~/my-project

Run ./scripts/install-skills.sh --help for the full set of options. Common ones:

Verification Workflow

KVerus is organized as a set of composable skills for turning Rust code into verified Verus code. The recommended entrypoint is kverus-run, whi