KVerus is a skill-based workflow for migrating Rust code to formally verified Verus, adding specifications and proofs, repairing verification failures, and auditing the result. Use the skills individually or run the full pipeline with kverus-run.

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

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

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

# sync python environment
$ uv sync

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

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

# Or on Windows PowerShell:
> .\scripts\install-skills.ps1 ~\my-project

The installer supports copy or symlink mode, Codex and Claude Code targets, selective skill installation, and overwriting existing installations. Run it with --help for details.

The recommended entrypoint is the end-to-end pipeline:

$kverus-run target=path/to/file_or_dir verify="<verification command>"

target can be a single .rs file or a directory of Rust files. verify should be the exact command used by the target project to run Verus verification, for example a project-specific cargo verus ... or wrapper command. If out_dir is not provided, kverus-run writes reports under .kverus-run-output/.

Rust code
  -> kverus-migrate
  -> kverus-spec
  -> kverus-fix
  -> kverus-eval
  -> kverus-semantic-audit
  -> kverus-postprocess
       -> kverus-strip
  -> verified Verus code + reports

The pipeline migrates Rust to Verus, adds and repairs proofs, evaluates their quality, audits executable semantics, and performs final cleanup. See the skills reference for details. The final report is written to <out_dir>/pipeline_summary.md.

Individual stages can also be invoked for targeted work. See the skills reference and the corresponding SKILL.md for their inputs and constraints.

The verified insertion sort is an end-to-end example from Rust code to verified Verus code, including source files, generated proofs, reproduction commands, and verification results.

KVerus has been used in VOSTD, the Asterinas system verification project. The VOSTD pull requests labeled AI-assist were developed using KVerus, with some implemented entirely by KVerus.

asterinas/vostd#395 demonstrates the core KVerus workflow on sync::rwmutex, taking the implementation from Rust code to fully verified Verus code. The following commits capture the intermediate migration and verification results:

This case focuses on the three core stages: migration, specification, and verification repair. The commits are reference outputs for demonstrating the skills rather than boundaries for the full kverus-run pipeline.

asterinas/vostd#633 demonstrates kverus-strip on specs::mm::page_table::cursor::cursor_steps. The skill simplified a single Rust source file, removing 1,075 lines of redundant proof code while keeping verification passing.

This showcase uses tree-sitter-verus for full proof-call discovery. Before starting the agent, install the repository's Python dependencies.

If you find KVerus useful in your research, please consider citing our ASE 2026 paper:

@inproceedings{10.1145/3832783.3834503,
  author = {Liu, Yuwei and Wan, Xinyi and Wang, Yanhao and Wang, Minghua and Huang, Lin and Wei, Tao},
  title = {KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code},
  year = {2026},
  isbn = {9798400728822},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3832783.3834503},
  doi = {10.1145/3832783.3834503},
  booktitle = {Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering},
  pages = {4139–4151},
  numpages = {13},
  keywords = {Formal Verification, Large Language Models, Proof Generation, Rust, Verus},
  location = {Munich, Germany},
  series = {ASE '26}
}