makecindy
Featured
cindy
Cindy is an open-source AI agent that runs locally on your machine, integrates multiple AI harnesses and models, and provides memory, skills, and automation to perform real work in your projects and apps.
AI repository intelligence
FR-AI / ANALYSISWhy it is worth attention
It provides a composable, end-to-end pipeline for formal verification of Rust code, demonstrated on real-world system code (VOSTD) and presented at ASE 2026.
Who it is for
- Rust developers seeking formal verification
- Researchers in program verification
- System programmers working with Verus
- Developers of verified operating systems
Use cases
- Migrating existing Rust code to a Verus-compatible baseline
- Adding proof-oriented specifications and invariants
- Fixing verification failures without weakening specifications
- Stripping redundant proof code while keeping verification passing
Strengths
- Composable skills allow stage-by-stage or full pipeline use
- Includes semantic audit to ensure executable behavior matches original Rust
- Proven on VOSTD (Asterinas system verification) with real pull requests
- kverus-strip removed 1,075 lines of redundant proof code in a showcase
Considerations
- Requires Verus toolchain installation
- Python environment needed for accurate parsing (with LLM-based fallback)
- Intended for use with agent tools (Codex or Claude Code) requiring external API access
README quick start
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-stripusestreesitter-verusto parse Verus code more precisely, but it can also fall back to an LLM-based path without it. If you do not use an accuratekverus-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:
| Option | Description |
|---|---|
-m, --mode | symlink (default) or copy |
-t, --targets | agent, claude, or both (default: agent) |
-s, --skills | Comma-separated skill names (default: all) |
-f, --force | Overwrite existing installations |
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
Description
KVerus: Scalable and Resilient Formal Verification for Rust Code
Related repositories
Similar projects matched by category, topics, and programming language.
uzairansaruzi
Featured
hermex
Hermex is a native SwiftUI iPhone app that lets you control a self-hosted Hermes AI agent directly from your phone, with no subscriptions, tracking, or third-party relay.
hahhforest
Featured
pi-textbook
A hands-on course that walks through building a Pi-style coding agent from scratch across 15 checkpoints, starting from an offline agent trajectory.