Loading ToolBench
HTTP MCP front-end for F*'s IDE protocol, providing tools for F* session management, typechecking, symbol lookup, and proof state inspection.
F* MCP server has well-structured tool definitions with complete JSON schemas and descriptions for all 8 tools. Naming follows verb_noun convention (create_session, typecheck_buffer, etc.). However, descriptions are generic and lack LLM-optimization guidance on WHEN to use each tool vs alternatives. Parameter descriptions exist but are minimal (10-30 chars typical). Output schemas are not documented, callers cannot see what fields to expect from responses. Error handling is basic; no recovery guidance or actionable error messages visible in tool definitions. Session management via lazy_static SESSION_MANAGER is functional but introduces stateful server behavior contrary to current MCP spec (2026-07-28) which emphasizes stateless request handling.
Close an F* session and kill its process.
Create a new F* session. All arguments are optional with sensible defaults.
Get proof goals and context at a given line from the last typecheck.
List all active F* sessions with their status and metadata.
Look up a symbol or module at a given position in the code.
Restart the Z3 SMT solver in the F* session.
Typecheck F* code in a session. Supports full and lax typechecking modes.
Output schemas not documented. Tool descriptions state what they do but do not specify return value structure. LLMs cannot plan downstream calls or extract required fields (e.g., what fields does list_sessions return? Is there pagination?). Callers must infer structure from implementation.
Descriptions lack LLM-optimization guidance. Generic descriptions like 'Look up a symbol or module at a given position in the code' do not explain WHEN to call this vs other tools, what prerequisites exist, or what the typical workflow is. Descriptions should be 50-200 chars and answer: what, when, why.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 54 | <=2025-11-25 | v2 |
Add a file to F*'s virtual file system.
Stateful session management via lazy_static SESSION_MANAGER violates MCP 2026-07-28 stateless request handling principle. Server maintains mutable session state across requests without per-request _meta context. Current spec requires each request to be self-contained; stateful initialize/Mcp-Session-Id pattern is removed.
No error recovery guidance in tool definitions. Error handling code exists (session_not_found_error helper) but tool descriptions do not document what errors are possible, whether they are retryable, or what the LLM should do next.
Parameter descriptions are minimal (10-30 chars). E.g., 'The F* session ID' for session_id, 'F* code to typecheck' for code. Descriptions should include format hints, constraints, and examples. E.g., 'Session ID (UUID format, returned by create_session). Required.'