Formal verification of Rust code with AI-assisted specification and proof. Multi-framework, multi-runtime.
npx fv-skills-baifWorks on Mac, Windows, and Linux. Supports Claude Code, Codex, OpenCode, and Gemini CLI.
FVS encodes the expert formal verification workflow into skills for AI coding assistants. It takes Rust code through a structured pipeline — dependency analysis, deep code understanding, specification generation, and proof — using the AI to handle the tedious parts while you stay in control of the verification strategy.
v1 focuses on Lean 4 via Aeneas (Rust → Charon → LLBC → Aeneas → Lean 4). Cross-language porting from Verus, F*, Coq, and Dafny is supported via /fvs:lean-spec-port and /fvs:lean-proof-port.
Some capabilities are framework-agnostic and work regardless of your verification target:
- Dependency mapping builds function call graphs from any extracted code
- Verification planning picks optimal targets using greedy graph traversal
- Natural language explanation produces human-readable summaries of Rust functions with pre/post conditions
Framework-specific commands (currently Lean) handle the actual specification and proof generation.
npx fv-skills-baifThe installer prompts you to choose:
- Runtime — Claude Code, OpenCode, Gemini, or all
- Location — Global (all projects) or local (current project only)
Verify with /fvs:help inside your chosen runtime.
- A Lean 4 project with
lakefile.tomlandlean-toolchain - Aeneas-generated output (
Types.lean,Funs.lean) from your Rust source - Lean 4 toolchain installed and working
For enhanced Lean 4 proof development with LLMs, install the lean-lsp-mcp server. It provides instant goal state checking, local lemma search, and proof diagnostics without rebuilding.
Note: Avoid using the lean_multi_attempt tool for formal verification tasks - FV proof states often explode in size, making multi-attempt testing prohibitively slow.
npx fv-skills-baif@latestNon-interactive Install (Docker, CI, Scripts)
# Claude Code
npx fv-skills-baif --claude --global # Install to ~/.claude/
npx fv-skills-baif --claude --local # Install to ./.claude/
# Codex
npx fv-skills-baif --codex --global # Install to ~/.codex/
# OpenCode
npx fv-skills-baif --opencode --global # Install to ~/.config/opencode/
# Gemini CLI
npx fv-skills-baif --gemini --global # Install to ~/.gemini/
# All runtimes
npx fv-skills-baif --all --global # Install to all directoriesUse --global (-g) or --local (-l) to skip the location prompt.
Use --claude, --codex, --opencode, --gemini, or --all to skip the runtime prompt.
| Command | Description |
|---|---|
/fvs:map-code |
Build function dependency graph from extracted code and Rust source |
/fvs:plan |
Pick next verification targets via greedy dependency graph traversal |
/fvs:natural-language |
Generate natural language explanation of module or function with pre/post conditions |
/fvs:help |
Show available FVS commands and usage guide |
/fvs:update |
Self-update to latest version via npx |
/fvs:reapply-patches |
Reapply local modifications after an FVS update |
/fvs:sync-aeneas |
Sync Aeneas upstream documentation and update FVS references |
| Command | Description |
|---|---|
/fvs:lean-specify |
Generate Lean spec skeleton with @[step] theorem pattern |
/fvs:lean-verify |
Attempt proof using domain tactics (step, simp, ring, agrind, scalar_tac) |
/fvs:lean-refactor |
Refactor, simplify, and decompose verified proofs (dead code removal, simp sharpening, tactic golf) |
| Command | Description |
|---|---|
/fvs:lean-spec-port |
Port specs from other FV languages (Verus, F*, Coq, Dafny) to Lean |
/fvs:lean-proof-port |
Port proofs from other FV languages to Lean |
| Command | Description |
|---|---|
/fvs:lean-formalise |
Formalise paper/math content into Lean 4 specs and definitions |
/fvs:kb-setup |
Set up NotebookLM knowledge base integration (venv, auth, config) |
FVS follows a five-stage workflow. Each stage builds on the previous.
/fvs:map-code — Analyze extracted code and Rust source to build a function dependency graph. Produces CODEMAP.md with every function, its dependencies, and verification status. Works with any extraction pipeline.
/fvs:plan — Walk the dependency graph bottom-up to find optimal verification targets. Prioritizes leaf functions (no unverified dependencies) using greedy traversal. Performs deep Rust source analysis to reason about pre/post conditions and bounds.
/fvs:lean-specify <function> — Generate a specification skeleton for the target function. For Lean 4: uses the @[step] theorem fn_spec pattern with preconditions from Rust source analysis and postconditions matching function behavior.
/fvs:lean-verify <function> — Attempt to prove the specification. For Lean 4: uses domain-specific tactics (step, simp, ring, field_simp, omega). Reports proof status and remaining goals if incomplete.
/fvs:lean-refactor <spec_path> — Refactor, simplify, and decompose verified proofs. Applies tiered heuristics (dead code removal, simp sharpening, tactic golf, smart automation) while verifying compilation after every change. Three modes: safe, balanced (default), and aggressive.
# Global
npx fv-skills-baif --claude --global --uninstall
npx fv-skills-baif --opencode --global --uninstall
# Local (current project)
npx fv-skills-baif --claude --local --uninstallRemoves all FVS commands, agents, hooks, and settings entries. Does not affect other installed tools.
FVS builds on the work of several open-source projects:
-
Aeneas -- FVS incorporates and adapts documentation and proof skills from the Aeneas verification framework (Apache 2.0). The upstream Aeneas documentation is stored in
fv-skills/upstream/aeneas/and can be synced with/fvs:sync-aeneas. -
GSD (Get Shit Done) -- FVS follows the GSD plugin architecture for Claude Code skill distribution (MIT).
-
lean-lsp-mcp -- MCP server for Lean LSP integration, referenced in proof workflows (MIT).
MIT License. See LICENSE for details.