# Verum Axiom AI MCP for Claude and Codex **URL:** \ **Category:** AI - Corner\ **Created:** [October 15, 2026, 11:08am UTC](https://forum.verum.com/t/verum-axiom-ai-mcp-for-claude-and-codex/1121 "2026-10-15T11:08:35Z")\ **Posts on this page:** 3\ **Page:** 1
**Author:** ![geeksforgeeks](https://avatars.discourse-cdn.com/v4/letter/g/59ef9b/32.png) [@geeksforgeeks](https://forum.verum.com/u/geeksforgeeks)\ **Post date:** [October 15, 2026, 11:08am UTC](https://forum.verum.com/t/verum-axiom-ai-mcp-for-claude-and-codex/1121/1 "2026-10-15T11:08:35Z")
With `axiom ai mcp` an AI coding agent can check, verify and simulate the Verum Axiom models it writes. Part 1 is the same for every agent; Part 2 covers Claude Code, Claude Desktop, Codex and GitHub Copilot. > **About paths in this guide:** `` is the folder that holds the `axiom` program, and `` is the program itself. For example: > > - **macOS:** folder `/Library/VerumAxiom`, program `/Library/VerumAxiom/axiom` > - **Linux:** folder `/opt/VerumAxiom`, program `/opt/VerumAxiom/axiom` > - **Windows:** folder `C:\Tools\axiom`, program `C:\Tools\axiom\axiom.exe` > > Replace them with the folder where you installed Verum Axiom. On Windows, JSON and TOML files need each backslash doubled: `C:\\Tools\\axiom\\axiom.exe`. # Part 1. General ## Add the server `axiom ai mcp` is a local MCP server (stdio). The agent starts it and runs its tools on the `.dzn` files it writes, so the agent must run on your machine and be able to write files. You need a Verum Axiom version that includes `axiom ai mcp`. Register this command with your agent (Part 2 shows where): ```auto ai mcp ``` - Always give the full path: the program is not on your `PATH`. - The program is the first word; `ai` and `mcp` are its two arguments. A form with separate fields for the command and the arguments wants them apart: only the program in the command field. - **Windows:** the program is `axiom.exe`. An agent running in WSL is a Linux program: it needs the Linux build of Verum Axiom, not the Windows one. - A tool call stops after 600 seconds. For large designs, add `--timeout 1800`. - The agent loads the server when a session starts: start a new session after adding it. ### Where the setting lives | Where | Use for | Claude Code | Codex | Copilot Chat | | --- | --- | --- | --- | --- | | This project, only you | Trying it out | no `--scope` (the default) | `.codex/config.toml`, kept on your machine only | `.vscode/mcp.json`, kept on your machine only | | Every project, only you | Daily use | `--scope user` | `~/.codex/config.toml` | user configuration | | This project, the whole team | A shared repository | `--scope project` (`.mcp.json`) | `.codex/config.toml`, shared through the repository | `.vscode/mcp.json`, shared through the repository | On Windows, `~/` is your profile folder (`%USERPROFILE%\`) and paths use `\`. A team file runs only after each user approves or trusts it once. ### Approve it The first time, your agent asks you to trust the server and to allow its tools. The Verum Axiom tools only read your models and check them; the agent writes the `.dzn` files with its own editing tools, which keep asking as you have set them to. In Claude Code you can allow all Verum Axiom tools at once (Part 2). ## Check it > **macOS and Linux** > > Test the server on its own, in a terminal. This should list its eight tools: > > ```auto > printf '%s\n' \ > '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2024-11-05","capabilities":{},"clientInfo":{"name":"p","version":"0"}}}' \ > '{"jsonrpc":"2.0","method":"notifications/initialized"}' \ > '{"jsonrpc":"2.0","id":2,"method":"tools/list","params":{}}' | ai mcp > > ``` > **Windows** > > Test the server on its own: start it in PowerShell. It should print nothing and wait for an agent; press Ctrl+C to stop it. If it prints an error and exits, your agent cannot start it either. > > ```auto > & "" ai mcp > > ``` Then, in a new session, ask your agent: _Which Verum Axiom tools do you have?_ It should name the eight tools below. Part 2 has each agent’s own check. ## Tools | Tool | What it does | | --- | --- | | `guide` | The modelling guide, by topic | | `check` | Parse and well-formedness errors, with a fix for common mistakes | | `verify` | Deadlock, livelock, illegal, compliance and invariants, each failure located | | `simulate` | Replays a trace: accepted, or where and why it is rejected | | `explore` | Drives a model one choice at a time | | `evidence` | Replays every requirement’s traces from `requirements.json` | | `review` | Design faults verify cannot see, such as unreachable parts or copied port state | | `equivalent` | Whether two versions behave the same on all ports | ## How the agent works The server tells the agent the order of work, so a plain request is enough: 1. It shows you the numbered requirements and asks whether they are complete. 2. It asks about gaps one question per message, each with a suggested answer, and waits for you. 3. It writes interfaces and small components, running `check`, `verify` and `review`. 4. It writes `requirements.json` with a must-happen and a must-not-happen trace per requirement, and runs `evidence` until all pass. 5. It reports the model, the evidence and the choices it made. > **Scripts and CI.** Each agent can run a single prompt without a person: > > - Claude Code: `claude -p ""` > - Codex: `codex exec ""` > - GitHub Copilot CLI: `copilot -p ""` > > With no one to answer, the agent stops at its first question. Add `No one will answer questions in this session.` to the prompt. > > Also give permission in advance for the Verum Axiom tools and for writing files: with no one to approve them, the run cannot use them. ## Use it ### Your first model 1. **Start.** Make an empty folder, add the server there, and start your agent. 2. **Check the connection.** Confirm the agent has the Verum Axiom tools (see _Check it_). 3. **Describe what you want** in plain words: ```auto I want a model of a lamp with a switch. Pressing the switch turns the lamp on; pressing it again turns it off. The lamp reports when it is lit. ``` 1. **Check the list.** The agent shows the requirements it read, numbered, and asks whether they are complete. Add what is missing and remove what is wrong. 2. **Answer the questions.** A description in words always leaves things open: what happens when the switch is pressed while the lamp is still switching, whether the lamp starts on or off. The agent asks one question at a time, with a suggested answer; confirm it or give your own. Your answers become requirements, so the model is the one you meant rather than a plausible guess. 3. **Watch the work.** The agent reads the guide, writes `.dzn` files, runs `check` and `verify` until they pass, then writes `requirements.json` and runs `evidence`. 4. **Read the report:** the files, one sentence per component, the evidence, and the choices it made. Ask about any choice you did not make yourself. ### Ask well - **Give fixed interfaces verbatim** and say they must not change. - **Read the requirement list critically.** Agents tend to miss the client’s contract and the hardware’s rules. - **On an existing model, say which job it is:** restructuring (proved with `equivalent`) or extending (old requirements must still hold). - **Name folders the models import from.** ### Read the result - `verify`: `OK`, or `FAIL : , at event n` with the location. - `evidence`: each requirement is `evidenced`, `explained` (an invariant covers it), `MISSING` or `FAILING`. Notes mark traces that show little. - `review`: errors are faults; warnings ask whether a design choice is meant. ### Know the limits A clean `verify` shows the model is sound, not that it matches your specification, and the agent writes its evidence from its own model. Check the requirement list and a few traces yourself, or ask the agent to `explore` the model with you. ## Troubleshooting | Problem | Fix | | --- | --- | | The server does not start | Check the folder in the command; run the test in _Check it_. | | Enabled, but the agent has no Verum Axiom tools | The whole command went into one field. Put only the program in the command field; `ai` and `mcp` are arguments. | | `ai` is an unknown command | Verum Axiom is too old. Update it. | | **macOS:** macOS blocks the server | Files copied from a `.dmg` or a download are quarantined. Run `xattr -dr com.apple.quarantine ` | | **Linux:** “Permission denied” | The files lost their execute bit when they were copied. Run `chmod +x /mcrl2/bin/*` | | **Windows:** fails with a macOS or Linux path such as `/Library/VerumAxiom` | A command copied from another system. Use the Windows folder; the program is `axiom.exe`. | | **Windows:** a configuration file stops loading after adding the path | JSON and TOML need each backslash doubled: `C:\\Tools\\axiom\\axiom.exe`. | | **Windows:** Windows blocks the program, or SmartScreen warns | Files from a download are marked as coming from the internet. In PowerShell: `Get-ChildItem "" -Recurse | Unblock-File` | | Long `verify` calls stop | Add `--timeout 1800`, and raise your agent’s own limit (Part 2). | | No change after updating Verum Axiom | Start a new agent session. | # Part 2. Per agent ## Claude Code ### Add the server In a terminal, inside your project: ```auto claude mcp add axiom -- ai mcp ``` - **Scope:** add `--scope user` or `--scope project` after `add` (see _Where the setting lives_). - **VS Code extension only?** There is no `claude` on your `PATH`. Use `~/.vscode/extensions/anthropic.claude-code--/resources/native-binary/claude` (macOS and Linux) or `%USERPROFILE%\.vscode\extensions\anthropic.claude-code--\resources\native-binary\claude.exe` (Windows), or install the CLI: `npm install -g @anthropic-ai/claude-code`. ### Check it Start a new session (in VS Code: _Developer: Reload Window_), then: ```auto claude mcp list ``` It should show `axiom` as **Connected**. Inside a session, `/mcp` lists its eight tools. ### Options - **No instructions file needed:** Claude Code puts the server’s instructions in its system prompt. - **Allow all Verum Axiom tools** without being asked each time, in `.claude/settings.json`: ```auto { "permissions": { "allow": ["mcp__axiom"] } } ``` ### Troubleshooting | Problem | Fix | | --- | --- | | `claude mcp list` says Connected, `/mcp` does not show it | Start a new session. | | Pending approval | Start a session in the project and approve `.mcp.json`. | | Failed to connect | Wrong folder in the command. To fix it, run `claude mcp remove axiom` (with the same `--scope`) and add it again. | | Missing from `claude mcp list` | Added in another project: without `--scope`, a server belongs to the folder you added it in. Run the command inside this one, or add it with `--scope user`. | ## Claude Desktop > **Linux:** Anthropic does not publish the Claude desktop app for Linux. On Linux, use Claude Code. ### Add the server In the Claude app, open **Settings** , **Developer** , **Edit Config**. It opens `claude_desktop_config.json`, found for you. Add `axiom` inside `mcpServers`; if the file already has other servers or settings, keep them: > **macOS** > > File: `~/Library/Application Support/Claude/claude_desktop_config.json` > > ```auto > { > "mcpServers": { > "axiom": { > "command": "/Library/VerumAxiom/axiom", > "args": ["ai", "mcp"] > } > } > } > > ``` > > Then quit the app completely: closing the window leaves it running. Choose **Claude** , **Quit Claude** in the menu bar (or press Cmd+Q), and start it again. > **Windows** > > File: `%APPDATA%\Claude\claude_desktop_config.json`, or a folder under `%LOCALAPPDATA%\Packages` for the Microsoft Store app. > > ```auto > { > "mcpServers": { > "axiom": { > "command": "C:\\Tools\\axiom\\axiom.exe", > "args": ["ai", "mcp"] > } > } > } > > ``` > > Then quit the app completely: closing the window leaves it running. Right-click the Claude icon in the system tray, choose **Quit** , and start it again. Use your own path in `"command"`. ### Give it a folder The chat cannot write files on its own, and every Verum Axiom tool reads a `.dzn` file. Open **Settings** , **Extensions** , install **Filesystem** , and allow one folder for your models. The server starts in a folder you do not choose, so tell Claude where to work and to use full paths, for example: _Work in /Users/me/axiom-models and give every Verum Axiom tool the full path._ (Windows: _Work in C:\Users\me\axiom-models …_) ### Check it **Settings** , **Developer** should show `axiom` as **running**. In a new chat, ask: _Which Verum Axiom tools do you have?_ The app’s **Code** tab is Claude Code: it uses the setting from _Claude Code_, not this file. ### Troubleshooting | Problem | Fix | | --- | --- | | **macOS:** not listed after editing the file | Quit from the menu bar (Cmd+Q), not by closing the window, and start the app again. | | **Windows:** not listed after editing the file | Quit from the system tray, not by closing the window, and start the app again. | | **macOS:** shows failed | Open its logs folder from **Settings** , **Developer** ; `mcp-server-axiom.log` says why. Usually a wrong folder. | | **Windows:** shows failed | Open its logs folder from **Settings** , **Developer** ; `mcp-server-axiom.log` says why. Usually a wrong folder or single backslashes in the JSON. | | Claude has the tools but writes no files | Install the Filesystem extension and allow your models folder. | | A tool cannot find the model | Give it the full path to the `.dzn` file. | ## Codex ### Add the server The Codex app tab, CLI and IDE extension all read `~/.codex/config.toml` (Windows: `%USERPROFILE%\.codex\config.toml`). Add: ```auto [mcp_servers.axiom] command = "" args = ["ai", "mcp"] startup_timeout_sec = 20 tool_timeout_sec = 600 ``` (On Windows, double the backslashes in `command`, e.g. `"C:\\Tools\\axiom\\axiom.exe"`.) - Or run `codex mcp add axiom -- ai mcp` and add the two timeout lines by hand. Without `tool_timeout_sec`, Codex may stop a long `verify` early. If you add `--timeout` to the server, set `tool_timeout_sec` to at least the same value. - For one project, use `.codex/config.toml` there; Codex reads it only if the project is trusted. - **Windows:** Codex running inside WSL reads its own `~/.codex/config.toml` in Linux, and needs the Linux build of Verum Axiom. Native Windows Codex is the simpler setup. **In the Codex app** you can use its form instead: **Settings** , **Plugins** , **MCPs** , **Add**. It writes the same file. | Field | Value | | --- | --- | | Command to launch | ``, and nothing after it | | Arguments | `ai`, then **Add argument** and `mcp` | | Environment variables | none | | Working directory | empty, or your models folder | ### Check it ```auto codex mcp list ``` It should show `axiom` as **enabled**. Enabled means it is switched on, not that it starts: start a new session and ask: _Which Verum Axiom tools do you have?_ In the Codex app, start a new chat inside a project; a chat keeps the tools it had when it began. ### Tell it what Verum Axiom is Codex gets the server’s tools but not its instructions, and to a model “an axiom model” can mean logic: asked for one, Codex may write axioms as formulas instead of a `.dzn` file. Put this in `AGENTS.md` in your project folder; Codex reads it in every session there: ```auto Models in this project are Verum Axiom (Dezyne) `.dzn` files. Use the axiom MCP tools: call `guide` (topic: workflow) first, write the model to a `.dzn` file, then `check` and `verify` it. Never describe a model in prose instead of writing the file. ``` - Use medium or high reasoning effort. At the lowest settings Codex may answer without trying a tool. - ChatGPT’s ordinary chat cannot use the server: it cannot start local programs or write your files. ### Troubleshooting | Problem | Fix | | --- | --- | | Missing from `codex mcp list` | Check the file and the header `[mcp_servers.axiom]`. | | Listed, but no Verum Axiom tools | Start a new session; trust the project for a project file. | | Enabled in the app, but Codex says it has no Verum Axiom tools | Open the server’s settings (the gear): if _Command to launch_ holds `ai mcp` too, move them to _Arguments_. Then start a new chat; an existing one, even moved into a project, keeps its old tools. | | Answers with formulas or a table, not a `.dzn` file | Add `AGENTS.md` (above), or say _use the axiom tools_ in the request. | | **Windows:** configuration ignored after adding the path | Backslashes in a TOML `"…"` string must be doubled. | | “Startup timed out” | Raise `startup_timeout_sec`; check the folder in `command`. | ## GitHub Copilot ### Add the server **Copilot Chat in VS Code:** run **MCP: Add Server** , choose **Command (stdio)**, paste the command from _Add the server_, and name it `axiom`. Or edit `mcp.json` yourself ( **MCP: Open User Configuration** , or `.vscode/mcp.json` for the team): ```auto { "servers": { "axiom": { "type": "stdio", "command": "", "args": ["ai", "mcp"] } } } ``` (On Windows, double the backslashes in `command`.) **Copilot CLI:** ```auto copilot mcp add axiom -- ai mcp ``` The CLI keeps servers in `~/.copilot/mcp-config.json` (Windows: `%USERPROFILE%\.copilot\mcp-config.json`), which Copilot Chat in VS Code does not read. The two files differ: VS Code’s has `"servers"` and `"type": "stdio"`, the CLI’s has `"mcpServers"` and `"type": "local"`. ### Check it - Run **MCP: List Servers** , start `axiom` and trust it. - Open Copilot Chat in **Agent** mode, with `axiom` ticked in the tools picker, and ask: _Which Verum Axiom tools do you have?_ ### Options - If Copilot skips steps of _How the agent works_, write them in `.github/copilot-instructions.md`; Copilot reads it in every chat. - Copilot’s cloud agent on [github.com](http://github.com) runs on Linux and needs a Linux build of Verum Axiom. ### Troubleshooting | Problem | Fix | | --- | --- | | “MCP servers are disabled by your organization” | Your Copilot comes from a GitHub organization or enterprise that turns MCP off; Business and Enterprise plans start with it off. An owner sets **Settings** , **Copilot** , **Policies** , **MCP servers in Copilot** to Enabled, for every organization that gives you Copilot (or at the enterprise, which overrides them). Then sign out of GitHub in VS Code, run **Developer: Reload Window** and sign in again: VS Code reads the policy when you sign in. | | Not in MCP: List Servers | Add it to VS Code’s `mcp.json`, not the CLI’s file. | | Server shows Error | Open **Output** , **MCP: axiom** ; usually a wrong folder. | | No Verum Axiom tools in chat | Switch to Agent mode and tick `axiom` in the tools picker. | | Long `verify` stops | Copilot may stop calls early; verify one model at a time. | * * * ---
**Author:** ![Bird](https://dub1.discourse-cdn.com/flex017/user_avatar/forum.verum.com/bird/32/18_2.png) [@Bird](https://forum.verum.com/u/Bird)\ **Post date:** [October 15, 2026, 11:40am UTC](https://forum.verum.com/t/verum-axiom-ai-mcp-for-claude-and-codex/1121/4 "2026-10-15T11:40:28Z")
---
**Author:** ![Bird](https://dub1.discourse-cdn.com/flex017/user_avatar/forum.verum.com/bird/32/18_2.png) [@Bird](https://forum.verum.com/u/Bird)\ **Post date:** [October 15, 2026, 11:41am UTC](https://forum.verum.com/t/verum-axiom-ai-mcp-for-claude-and-codex/1121/5 "2026-10-15T11:41:21Z")