Atelier B MCP 服务器

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.

Works with Atelier B Community Edition 24.04.2 (ATELIER B (Community Edition) version 24.04.2, B Compiler version/24.08), which is the version every tool is developed and tested against. Other 24.x releases are expected to work, since the server drives bbatch through its documented command names, but they are not tested. Commands available only in the Professional edition, vr (verify_rule) among them, are deliberately not exposed; see docs/coverage.md.

Also requires Python 3.11+ and mcp 2.0+.

History

Most recent first.

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. Files are returned exactly as they are on disk; when a PMI file is read, its per-PO entries are paired with the labels of the sibling PO file so they can be attributed to the right proof obligation (see docs/PMI_PMM_ORDERING.md).

Available Tools

Prerequisites

• Python 3.11+
• Atelier B Community Edition 24.04.2 with bbatch.exe (the tested version; see the note at the top)
• 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.