工作室B MCP服务器
一 MCP（模型上下文协议） 连接的服务器 克劳德·艾 随着 工作室B，形式化方法IDE为B方法。
此服务器使Claude能够直接与Atelier B项目交互：类型检查组件、生成证明义务、运行自动证明程序、生成C代码和管理项目文件。
建筑
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/ directories)服务器封装了Atelier B的 bbatch 命令行界面，将MCP工具调用转换为bbatch命令，并将输出解析回结构化响应。读取PMI/PMM文件时，它会自动为每个PO条目重新排序，以匹配bbatch的编号约定。
可用工具
| 类别 | 工具 |
|---|---|
| 项目管理 | atelierb_list_projects, atelierb_infos_project, atelierb_list_components, atelierb_create_project, atelierb_remove_project, atelierb_add_component, atelierb_remove_component |
| 验证 | atelierb_typecheck, atelierb_b0check, atelierb_pogenerate, atelierb_prove, atelierb_status |
| 代码生成 | atelierb_generate_c, atelierb_generate_project_c |
| 文件操作 | atelierb_list_files, atelierb_read_file, atelierb_write_file, atelierb_list_project_structure |
先决条件
- Python 3.11+
- 工作室B （社区版或专业版）
bbatch.exe - 克劳德桌面版 （或任何兼容MCP的客户端）
安装
# Clone the repository
git clone https://github.com/CLEARSY/atelierb-mcp.git
cd atelierb-mcp
# Install dependencies
pip install -e .
# Or install with dev dependencies
pip install -e ".[dev]"配置
复制 .env.example 并调整路径：
cp .env.example .env环境变量：
| 变量 | 描述 | 默认值 |
|---|---|---|
ATELIERB_PATH | B工作室安装路径 | C:\Program Files\Atelier B Community Edition 24.04.2 24.04.2 |
ATELIERB_WORKSPACE | B项目工作区路径 | *（无--必须设置）* |
ATELIERB_BBATCH_CMD | bbatch可执行文件名 | bbatch.exe |
ATELIERB_COMMAND_TIMEOUT | 命令超时（秒） | 120 |
重要提示： 您必须设置 ATELIERB_PATH 和 ATELIERB_WORKSPACE 以匹配您当地的Atelier B安装和B项目目录。
Claude桌面集成
添加到您的Claude Desktop配置(%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"
}
}
}
}调整 ATELIERB_PATH 和 ATELIERB_WORKSPACE 要匹配您的本地设置，请重新启动Claude Desktop。
使用示例
配置后，您可以询问Claude：
- *“列出工作区中的所有工作室B项目”*
- *“在SafetySystem项目中对气闸机进行类型检查”*
- *“对Airlock_i实现运行B0检查”*
- *“生成证明义务并在气闸上运行证明程序”*
- *“显示安全系统项目的证明状态”*
- *“为气闸组件生成C代码”*
发展
# 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项目结构
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这个项目是如何建造的
该项目是使用 克劳德代码 （Anthropic为克劳德设计的CLI）。整个代码库——服务器实现、工具、解析器、测试和文档——都是在开发计划和迭代改进的指导下，通过与Claude Code的交互式会话编写的。
文档
许可证
版权所有（C）2026 克利西
此程序是自由软件：您可以根据自由软件基金会发布的GNU Affero通用公共许可证的条款重新分发和/或修改它，无论是许可证的第3版，还是（由您选择）任何更高版本。
看 许可证.md 获取完整的许可证文本。