Plugins for F* proof-oriented programming, available for both GitHub Copilot CLI and Claude Code.
The canonical agent and skill files live under plugins/proof-copilot/ and are shared by both ecosystems. The Copilot CLI plugin reads plugin.json at the repo root, which points agents and skills at plugins/proof-copilot/agents/ and plugins/proof-copilot/skills/. The Claude Code plugin reads .claude-plugin/marketplace.json (also at the repo root), which advertises a single plugin sourced from ./plugins/proof-copilot/; that directory holds .claude-plugin/plugin.json plus the same agents/ and skills/ subdirectories. The 8 skill files are loaded by both ecosystems verbatim with no duplication.
| Agent | Description |
|---|---|
| fstar-coder | An expert F* and Pulse programmer that authors formal specifications, implements solutions, and proves correctness — all verified with fstar.exe. Handles both pure F* and Pulse (concurrent separation logic) uniformly. |
| Skill | Description |
|---|---|
| smtprofiling | Debug F* queries sent to Z3, diagnosing proof instability and performance issues. Includes a catalog of 10 proven stabilization techniques mined from real verification projects. |
| proofdebugging | Systematic workflows for debugging F*/Pulse verification failures — isolating failures, factoring lemmas, and hardening proofs. |
| fstarverifier | Verify F* and Pulse code with fstar.exe and interpret common error patterns. |
| specreview | Review F*/Pulse specifications for completeness, strength, and usability — catch weak postconditions and missing spec-impl connections. |
| fstarmcp | Use the F* MCP server for interactive, incremental typechecking — create a session once, then re-typecheck modified code without restarting F*. |
| projectsetup | Structure a new F*/Pulse verification project with Makefile and directory layout. |
| sourcebuild | Build F*, Pulse, and KaRaMeL from source (fstar2 branch). |
| krmlextraction | Extract verified F*/Pulse code to C via KaRaMeL. |
- F* — The agent can build F* from source using the
sourcebuildskill (requiresgit,opam/OCaml ≥ 4.14, andZ3). Alternatively, install a pre-built release from fstar-lang.org. Either way,fstar.exemust be on your PATH or configured viaFStar.fst.config.json. - Z3 — The SMT solver used by F*. The
sourcebuildskill can install the required versions automatically, or install alongside F* from a release. - Rust/Cargo (optional) — Required only for building the F* MCP server for incremental typechecking. See the
sourcebuildandfstarmcpskills.
Requires GitHub Copilot CLI.
copilot plugin install FStarLang/proof-copilotRequires Claude Code.
/plugin marketplace add FStarLang/proof-copilot
/plugin install proof-copilot@proof-copilot
You can invoke the agent in several ways:
-
Via the
/agentcommand — type/agentin an interactive session and selectfstar-coder. -
Naturally in a prompt — mention the agent by name:
Use the fstar-coder agent to implement a verified binary search -
Via command line:
copilot --agent=fstar-coder --prompt "Implement a verified binary search over a sorted sequence"
Skills are automatically invoked when relevant, or can be called directly:
Use the smtprofiling skill to diagnose why this proof is slow
Use the specreview skill to check if my postconditions are strong enough
Use the proofdebugging skill to isolate this verification failure
Use the fstar-coder agent to implement a verified binary search over a sorted sequence
Skills are invoked automatically when relevant, or explicitly:
Use the smtprofiling skill to diagnose why this proof is slow
Use the specreview skill to check if my postconditions are strong enough
Use the proofdebugging skill to isolate this verification failure
Future versions will add:
- smart context retrieval with vector embeddings
- enhanced spec review with provable tests
- support for other F*-related tools, EverParse, Kuiper, etc.
Apache 2.0 — see LICENSE.