Verum Axiom AI MCP for Claude and Codex

geeksforgeeks · October 15, 2026, 11:08am

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: <axiom-folder> is the folder that holds the axiom program, and <axiom> 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):

<axiom> 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:

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":{}}' | <axiom> 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.

& "<axiom>" 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:

It shows you the numbered requirements and asks whether they are complete.
It asks about gaps one question per message, each with a suggested answer, and waits for you.
It writes interfaces and small components, running check, verify and review.
It writes requirements.json with a must-happen and a must-not-happen trace per requirement, and runs evidence until all pass.
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 "<prompt>"

Codex: codex exec "<prompt>"

GitHub Copilot CLI: copilot -p "<prompt>"

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

Start. Make an empty folder, add the server there, and start your agent.
Check the connection. Confirm the agent has the Verum Axiom tools (see Check it).
Describe what you want in plain words:

   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.

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.
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.
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.
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 <model>: <check>, 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 <axiom-folder>`
Linux: “Permission denied”	The files lost their execute bit when they were copied. Run `chmod +x <axiom> <axiom-folder>/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 "<axiom-folder>" -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:

claude mcp add axiom -- <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-<version>-<platform>/resources/native-binary/claude (macOS and Linux) or %USERPROFILE%\.vscode\extensions\anthropic.claude-code-<version>-<platform>\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:

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:

{ "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

{
  "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.

{
  "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:

[mcp_servers.axiom]
command = "<axiom>"
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 -- <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	`<axiom>`, and nothing after it
Arguments	`ai`, then Add argument and `mcp`
Environment variables	none
Working directory	empty, or your models folder

Check it

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:

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):

{ "servers": { "axiom": { "type": "stdio", "command": "<axiom>", "args": ["ai", "mcp"] } } }

(On Windows, double the backslashes in command.)

Copilot CLI:

copilot mcp add axiom -- <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 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.

Topic		Replies	Views
Dezyne: Paving the Way to Practical Formal Software Engineering Verum Axiom	0	923	March 15, 2021
Dezyne 2.12.0 Release Announcements	0	432	April 21, 2021
Windows IDE binary error Known Issues	11	370	February 6, 2023
Automatic Lights: A Complex System with One-Button Deployment Tutorials	0	209	December 5, 2024
Dezyne 2.11.0 Release Announcements	0	349	March 3, 2021

Verum Axiom AI MCP for Claude and Codex

Part 1. General

Add the server

Where the setting lives

Approve it

Check it

Tools

How the agent works

Use it

Your first model

Ask well

Read the result

Know the limits

Troubleshooting

Part 2. Per agent

Claude Code

Add the server

Check it

Options

Troubleshooting

Claude Desktop

Add the server

Give it a folder

Check it

Troubleshooting

Codex

Add the server

Check it

Tell it what Verum Axiom is

Troubleshooting

GitHub Copilot

Add the server

Check it

Options

Troubleshooting

Related topics