Skip to main content
Glama
CLEARSY

Atelier B MCP Server

Official
by CLEARSY

atelierb_pogenerate

Generate proof obligations for a B component to verify its formal correctness. Optionally only generate new or changed proof obligations.

Instructions

Generate proof obligations for a B component

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
differentialNoIf true, only generate new/changed POs
project_nameYesName of the project
component_nameYesName of the component
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full burden of disclosing side effects. It only says 'Generate proof obligations' without indicating whether this writes files, overwrites existing POs, requires prior steps, or is destructive. This is a significant transparency gap for a generation tool.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is a single sentence, front-loaded with the action verb, and contains no fluff. It is appropriately sized for the straightforward purpose it conveys.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description is too sparse for a tool with no annotations and no output schema. It omits important context such as side effects, file output, prerequisites, and how the 'differential' flag fits into the workflow. The agent is left without enough information to understand the tool's full impact.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema provides descriptions for all three parameters (100% coverage), so the description does not need to add parameter-level detail. It adds no extra meaning beyond the schema, receiving the baseline score of 3.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('Generate'), the resource ('proof obligations'), and the scope ('for a B component'). It distinguishes from sibling tools like atelierb_prove (which proves the POs) and atelierb_typecheck (which type-checks), making the purpose unambiguous.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies usage when one wants to generate proof obligations, but it does not explicitly state when to use this tool versus alternatives, nor does it mention any prerequisites (e.g., a type-checked component) or exclusions. The context is clear but no direct guidance is provided.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Install Server

Other Tools

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/CLEARSY/atelierb-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server