Atelier B MCP Server

An MCP (Model Context Protocol) server that connects Claude AI with Atelier B, the formal methods IDE for the B-method.

This server enables Claude to directly interact with Atelier B projects: typechecking components, generating proof obligations, running the automatic prover, generating C code, and managing project files.

Architecture

Claude Desktop (MCP Client)
    |  MCP Protocol (stdio, JSON-RPC 2.0)
    v
MCP Server (Python)
    |  subprocess (stdin/stdout)
    v
bbatch.exe (Atelier B CLI)
    |  filesystem
    v
B Projects (bdp/ + lang/ + src/ directories)

The server wraps Atelier B's bbatch command-line interface, translating MCP tool calls into bbatch commands and parsing the output back into structured responses. When reading PMI/PMM files, it automatically reorders per-PO entries to match bbatch's numbering convention.

Available Tools

Category	Tools
Project Management	atelierb_list_projects, atelierb_infos_project, atelierb_list_components, atelierb_create_project, atelierb_remove_project, atelierb_add_component, atelierb_remove_component
Verification	atelierb_typecheck, atelierb_b0check, atelierb_pogenerate, atelierb_prove, atelierb_status
Code Generation	atelierb_generate_c, atelierb_generate_project_c
File Operations	atelierb_list_files, atelierb_read_file, atelierb_write_file, atelierb_list_project_structure

Prerequisites

• Python 3.11+
• Atelier B (Community Edition or Professional) with bbatch.exe
• Claude Desktop (or any MCP-compatible client)

Installation

# Clone the repository
git clone https://github.com/CLEARSY/atelierb-mcp.git
cd atelierb-mcp

All remaining commands are run from this repository root (the directory that contains pyproject.toml), not from the inner atelierb_mcp/ package directory.

Recommended: install into a virtual environment

On recent Linux distributions (and macOS with Homebrew Python), installing into the system interpreter fails with error: externally-managed-environment (PEP 668). Use a virtual environment:

python -m venv .venv

# Activate it
source .venv/bin/activate        # Linux / macOS
# .venv\Scripts\activate         # Windows (PowerShell / cmd)

# Install dependencies (run from the repository root)
pip install -e .

# Or install with dev dependencies
pip install -e ".[dev]"

Re-activate the environment (source .venv/bin/activate) in any new shell before running the server. When configuring an MCP client, point command at the interpreter inside .venv (for example .venv/bin/python) so it uses the installed dependencies.

Configuration

Copy .env.example and adjust paths:

cp .env.example .env

Environment variables:

Variable	Description	Default
ATELIERB_PATH	Path to Atelier B installation	C:\Program Files\Atelier B Community Edition 24.04.2 24.04.2
ATELIERB_WORKSPACE	Path to B projects workspace	(none -- must be set)
ATELIERB_BBATCH_CMD	bbatch executable name	bbatch.exe
ATELIERB_COMMAND_TIMEOUT	Command timeout in seconds	120

Important: You must set ATELIERB_PATH and ATELIERB_WORKSPACE to match your local Atelier B installation and B projects directory.

Claude Desktop Integration

Add to your Claude Desktop configuration (%APPDATA%\Claude\claude_desktop_config.json):

{
  "mcpServers": {
    "atelierb": {
      "command": "python",
      "args": ["-m", "atelierb_mcp.server"],
      "env": {
        "ATELIERB_PATH": "C:\\Program Files\\Atelier B Community Edition 24.04.2 24.04.2",
        "ATELIERB_WORKSPACE": "C:\\path\\to\\your\\B\\workspace"
      }
    }
  }
}

Adjust ATELIERB_PATH and ATELIERB_WORKSPACE to match your local setup, then restart Claude Desktop.

Usage Examples

Once configured, you can ask Claude:

• "List all Atelier B projects in the workspace"
• "Typecheck the Airlock machine in the SafetySystem project"
• "Run B0 check on the Airlock_i implementation"
• "Generate proof obligations and run the prover on Airlock"
• "Show the proof status of the SafetySystem project"
• "Generate C code for the Airlock component"

Development

# Run tests
pytest tests/ -v

# Run only unit tests (skip integration tests requiring bbatch)
pytest tests/ -v -m "not integration"

# Type checking
mypy atelierb_mcp/

# Linting
ruff check atelierb_mcp/

# Test with MCP Inspector
npx @modelcontextprotocol/inspector python -m atelierb_mcp.server

Project Structure

atelierb_mcp/
├── server.py              # MCP server entry point with tool definitions
├── bbatch_wrapper.py      # Async subprocess wrapper for bbatch CLI
├── parsers.py             # Output parsers for bbatch responses
├── config.py              # Pydantic settings management
└── tools/
    ├── project_tools.py   # Project management tools
    ├── proof_tools.py     # Verification tools (typecheck, prove, etc.)
    ├── file_tools.py      # File access tools
    └── code_tools.py      # C code generation tools

tests/
├── conftest.py            # pytest fixtures with mock bbatch
├── test_parsers.py        # Parser unit tests
└── test_bbatch_wrapper.py # Wrapper tests

docs/
├── ARCHITECTURE.md        # Detailed architecture documentation
├── DEPLOYMENT_GUIDE.md    # Step-by-step deployment instructions
└── bbatch_commands.md     # bbatch CLI command reference

How This Project Was Built

This project was developed using Claude Code (Anthropic's CLI for Claude). The entire codebase -- server implementation, tools, parsers, tests, and documentation -- was written through interactive sessions with Claude Code, guided by a development plan and iterative refinement.

Documentation

• Architecture - System architecture and design
• Deployment Guide - Step-by-step deployment instructions
• bbatch Commands - Atelier B CLI reference

License

Copyright (C) 2026 CLEARSY

This program is free software: you can redistribute it and/or modify it under the terms of the GNU Affero General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

See LICENSE.md for the full license text.