Atelier B MCP Server
OfficialServer Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| ATELIERB_PATH | No | Path to Atelier B installation | C:\Program Files\Atelier B Community Edition 24.04.2 24.04.2 |
| ATELIERB_WORKSPACE | Yes | Path to B projects workspace | |
| ATELIERB_BBATCH_CMD | No | bbatch executable name | bbatch.exe |
| ATELIERB_COMMAND_TIMEOUT | No | Command timeout in seconds | 120 |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": false
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| atelierb_list_projectsA | List all available Atelier B projects |
| atelierb_infos_projectB | Get detailed information about an Atelier B project |
| atelierb_list_componentsA | List all components (machines, refinements, implementations) in a project |
| atelierb_typecheckB | Typecheck a B component to verify syntax and type correctness |
| atelierb_b0checkA | B0 check a B component to verify it is B0 compliant (required before C code generation) |
| atelierb_pogenerateB | Generate proof obligations for a B component |
| atelierb_proveB | Run automatic prover on a B component. Force levels: 0-3 (auto), 10-13 (forced), -1 (fast), -2 (replay) |
| atelierb_statusB | Get proof status of a component or entire project |
| atelierb_list_filesA | List B source files in the workspace. Supports filtering by project and extension (.mch, .ref, .imp, .erf, etc.) |
| atelierb_read_fileA | Read the content of a B source file (.mch, .ref, .imp, etc.), C code (.c, .h), or Makefile from the workspace. Content is returned verbatim. For a .pmi file, a 'po_labels' list names the proof obligation each entry of its flat theories (ProofState, MethodList, PassList) belongs to; those entries carry no operation name of their own, so do not try to infer it from their position. |
| atelierb_write_fileA | Write or update the content of a B source file (.mch, .ref, .imp, etc.), C code (.c, .h), or Makefile in the workspace. Creates a backup by default. |
| atelierb_list_project_structureA | Get the directory structure of a B project showing files and subdirectories |
| atelierb_create_projectA | Create a new Atelier B project in the workspace with bdp, lang, and src subdirectories |
| atelierb_add_componentA | Add a new B component (machine, refinement, or implementation) to a project. Creates the file in src/ with a template and registers it with Atelier B. |
| atelierb_remove_componentA | Remove a component from an Atelier B project. Optionally delete the source file from disk. |
| atelierb_remove_projectA | Remove an Atelier B project. WARNING: If delete_files is true, permanently deletes all project files! |
| atelierb_generate_cA | Generate C code for a single B component (implementation or basic machine). Output goes to lang/c directory. |
| atelierb_generate_project_cA | Generate C code for a complete B project from a toplevel component. Output goes to lang/c directory. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 18 tools
Most tools target distinct resource-action pairs (project, component, proof, file, code generation). Potential confusion exists between infos_project and list_project_structure, and between list_files and list_components, but the descriptions are detailed enough to disambiguate.
All tools share the 'atelierb_' prefix, but the verb-noun pattern is inconsistent. 'infos_project' lacks a verb, 'status' is a bare noun, and 'b0check' and 'pogenerate' embed the object before the verb in an unusual way. A more uniform pattern like 'check_b0' or 'generate_po' would be clearer.
18 tools is at the high end (16-25 feels heavy). For a specialized B-method IDE, the count is understandable, but some read-only informational tools (infos_project, list_project_structure, list_files) could potentially be consolidated to reduce interface surface.
The tool set provides comprehensive lifecycle coverage: project and component CRUD, typecheck/B0 check, proof obligation generation/proving/status, file read/write, and C code generation for both components and entire projects. There are no major gaps in the B development workflow.