F* MCP Server

An MCP (Model Context Protocol) server that provides a front-end for F*'s --ide stdio protocol. This enables AI assistants to interact with F* for typechecking, symbol lookup, and other IDE features via the MCP standard.

Features

• Session Management: One session per file path with automatic replacement
• Full F IDE Protocol Support*: Typechecking, symbol lookup, and more
• Proof Context: Access proof obligations and goals during typechecking

Installation

# Build the server
cargo build --release

# Run the server
./target/release/fstar-mcp

MCP Tools

create_session

Create a new F* session. All arguments are optional with sensible defaults.

Parameters:

• file_path (string, optional): Path to the F* file. If omitted, creates a temporary .fst file.
• fstar_exe (string, optional): Path to fstar.exe. Defaults to 'fstar.exe' in PATH.
• cwd (string, optional): Working directory for F*. Defaults to the file's directory.
• include_dirs (array of strings, optional): Include directories (--include paths).
• options (array of strings, optional): F* command-line options (e.g., ['--cache_dir', '.cache']).

Returns:

{
  "session_id": "uuid",
  "status": "ok" | "error",
  "diagnostics": [...],
  "fragments": [...],
  "created_at": "2024-01-01T00:00:00Z"
}

list_sessions

List all active F* sessions with status information.

Parameters: None

Returns:

{
  "sessions": [...],
  "count": 2
}

typecheck_buffer

Typecheck code in an existing F* session.

Parameters:

• session_id (string): Session ID from create_session
• code (string): The F* code to typecheck
• lax (boolean, optional): If true, use lax mode (admits all SMT queries). Shortcut for kind='lax'
• kind (string, optional): Typecheck kind - "full", "lax", "cache", "reload-deps", "verify-to-position", "lax-to-position". Default: "full". Overridden by lax=true
• to_line (integer, optional): Line to typecheck to (for position-based kinds)
• to_column (integer, optional): Column to typecheck to (for position-based kinds)

Returns:

{
  "status": "ok" | "error",
  "diagnostics": [...],
  "fragments": [...]
}

update_buffer

Add or update a file in F*'s virtual file system (vfs-add).

Parameters:

• session_id (string): Session ID from create_session
• file_path (string): Path to the file in the virtual file system
• contents (string): Contents of the file

Returns:

{
  "status": "ok" | "error"
}

lookup_symbol

Look up type information, documentation, and definition location for a symbol.

Parameters:

• session_id (string): Session ID from create_session
• file_path (string): Path to the file containing the symbol
• line (integer): Line number (1-based)
• column (integer): Column number (0-based)
• symbol (string): The symbol to look up

Returns:

{
  "kind": "symbol" | "module" | "not_found",
  "name": "FStar.List.map",
  "type_info": "('a -> 'b) -> list 'a -> list 'b",
  "documentation": "...",
  "defined_at": {
    "file": "...",
    "start_line": 1,
    "start_column": 0,
    "end_line": 1,
    "end_column": 10
  }
}

get_proof_context

Get proof obligations and goals at a position. Returns proof states collected during last typecheck.

Parameters:

• session_id (string): Session ID from create_session
• line (integer, optional): Line number to get proof state at. If omitted, returns all proof states.

Returns:

{
  "found": true,
  "line": 10,
  "proof_state": {...}
}

Or when no line is specified:

{
  "count": 3,
  "proof_states": [...]
}

restart_solver

Restart the Z3 SMT solver for a session.

Parameters:

• session_id (string): Session ID from create_session

Returns:

{
  "status": "ok"
}

close_session

Close an F* session and clean up resources.

Parameters:

• session_id (string): Session ID from create_session

Returns:

{
  "status": "ok"
}

Development

# Run tests
cargo test

# Run with debug logging
RUST_LOG=fstar_mcp=debug cargo run

License

MIT