skills.rest
FStarLang
FStarLangOFFICIAL
Explore all skills by this author →
GitHub

fstarmcp

Typecheck F* and Pulse code incrementally via the fstar-mcp HTTP API.

8|4|Updated Mar 25, 2026
Search Tags:#mcp#pulse#fstar#typechecking#incremental verification#proof debugging
One-click install
npx skills add https://github.com/FStarLang/proof-copilot --skill fstarmcp
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: fstarmcp
Source: https://github.com/FStarLang/proof-copilot/tree/main/plugins/proof-copilot/skills/fstarmcp
Command: npx skills add https://github.com/FStarLang/proof-copilot --skill fstarmcp

SYSTEM DOCUMENTATION & REQUIREMENTS

What problem does it solve?

This Skill removes the friction of restarting F* during proof development by letting you typecheck, inspect, and iterate on code through the F* MCP server.

Core Features & Use Cases

  • Incremental Typechecking: Re-check modified F* or Pulse code without reloading the entire project, which is ideal for large verification workflows.
  • Session-Based Debugging: Create persistent sessions, inspect diagnostics, look up symbols, and restart the solver when proofs get stuck.
  • Project Integration: Configure Claude Code or GitHub Copilot CLI to connect to a local MCP server for interactive verification inside your development loop.

Quick Start

Tell the assistant to register the local F* MCP server for your project and use it to create a session for your target F* file so you can incrementally typecheck changes.

Frequently Asked Questions about fstarmcp

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I run incremental typechecking for F* without restarting the compiler?▼

You can run incremental typechecking by registering a JSON-RPC MCP server and creating a session for your target F* file, enabling live verification without restarting the compiler.

Can I debug stuck F* proofs interactively during a session?▼

Yes, session-based debugging allows you to inspect diagnostics, look up symbols, and restart the solver when F* proofs get stuck during large project verification workflows.

Does F* MCP work with Claude Code and GitHub Copilot CLI?▼

F* MCP works with Claude Code and GitHub Copilot CLI by configuring them to connect to your local MCP server for interactive verification inside your development loop.

What do I need to set up before using live typechecking for F* and Pulse code?▼

You need JSON-RPC MCP registration, local server configuration, and F* module paths that match the checked file structure to enable live typechecking for F* and Pulse code.

Why does my F* MCP session fail to verify modified Pulse code?▼

F* MCP verification fails if your F* module paths do not match the checked file structure, preventing the session from correctly inspecting symbols and applying incremental typechecking.

Related Skills

Explore More Software Engineering Skills→
v36372v36372

add-mcp-server

Configure global or project MCP servers in mcp.json for stdio or HTTP connections.

Community
Intermediate
MarioDeFelipeMarioDeFelipe
25

Flow Doctor

Diagnose and resolve errors in SAP Datasphere flows.

Community
Advanced
magicpro97magicpro97
8

template-skill

Coordinate Claude Code, Codex CLI, and GitHub Copilot CLI for task management and verification.

Community
Advanced
dotnetdotnet
1.2k

fsharp-diagnostics

Identify parse errors, type errors, and inferred type hints for modified F# sources.

Official
Intermediate