Loading ToolBench
MCP server for Frama-C formal verification with lazy spawn mode
Server has 10 tools with basic schemas and descriptions, but significant gaps limit production readiness. All tools have descriptions (10-150 chars, mostly adequate), and input schemas are present with type definitions. However, output schemas are entirely undocumented, LLMs cannot predict return structures. Parameter descriptions are minimal (1-2 sentences). No error handling guidance, no recovery paths, and no actionable error messages visible in code. Tool naming is verb-first (good), but several tools lack clarity on side effects and prerequisites. The lock/unlock pattern suggests state management concerns not addressed in descriptions. No tool annotations (readOnlyHint, destructiveHint, idempotentHint) despite clear risk levels (WRITE vs READ_ONLY). Composition is reasonable, tools chain logically (reload → list_functions → get_wp_goals → run_wp_prover → store_function_conclusion), but no documentation of this flow.
Add or update ACSL annotations (preconditions, postconditions, loop invariants) to a function
Retrieve the verification conclusion for a specific function, including meta.json and long-text fields from .md files
Retrieve the current project verification state from _program.json
Retrieve WP (weakest precondition) proof obligations for a function
List all functions in the current Frama-C project
Lock the project state to prevent concurrent modifications
Reload the Frama-C project from disk, spawning the main frama-c process if needed
No output schemas documented for any tool. LLMs cannot predict return structure, forcing them to guess at field names and types for downstream tool calls. This breaks tool chaining and increases hallucination risk.
No tool annotations (readOnlyHint, destructiveHint, idempotentHint) despite clear risk levels. Tools marked WRITE (reload_project, store_function_conclusion, run_wp_prover, add_annotation, lock_project, unlock_project) should declare destructiveHint=true to signal irreversibility to agents.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 52 | <=2025-11-25 | v2 |
Run the WP prover on a function to attempt automated proof of obligations
Store or update the verification conclusion for a function, persisting meta.json and long-text fields
Unlock the project state to allow modifications
lock_project and unlock_project lack clear descriptions of purpose, prerequisites, and side effects. What happens if an agent calls unlock without lock? Can concurrent agents deadlock? No guidance for error recovery.
store_function_conclusion has 5 parameters, 4 optional. No documentation of which combinations are valid, what happens if all are empty, or how partial updates interact with existing state. Undocumented parameter relationships invite misuse.
No error handling guidance visible. Tools like run_wp_prover (with timeout) and reload_project (spawning external process) can fail in multiple ways, but no recovery paths or actionable error messages documented.