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.

Related MCP server: BlenderMCP

Available Tools

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:

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.