MCP & CLI

Use Aristotle from your AI assistant through its MCP server, or from a terminal and in scripts with the CLI.

Set up the MCP

Add Aristotle's MCP server to your assistant, then sign in with your Aristotle account when it asks. There's no key to copy.

https://aristotle.harmonic.fun/mcp

Claude Code

claude mcp add --transport http --scope user aristotle https://aristotle.harmonic.fun/mcp

Then run /mcp and choose Authenticate.

Claude Desktop and claude.ai

Go to Customize › Connectors, add a custom connector with the server URL, and sign in. On Team and Enterprise plans, an Owner adds it under Organization settings › Connectors first.

ChatGPT

Where your plan allows custom MCP servers, go to chatgpt.com/plugins, add one with the server URL and OAuth, and sign in.

Codex

codex mcp add aristotle --url https://aristotle.harmonic.fun/mcp

Then sign in when Codex asks.

Cursor

Add this to ~/.cursor/mcp.json, then sign in when Cursor asks:

{
  "mcpServers": { "aristotle": { "url": "https://aristotle.harmonic.fun/mcp" } }
}

VS Code

Run MCP: Add Server, choose HTTP, enter the server URL, and sign in.

On a remote machine

If your assistant runs over SSH or in a cloud workspace, sign-in ends on a page with a curl command. Run it on the machine your assistant runs on.

Try it

Ask your assistant in plain words. For example:

• "Verify that the parser in ./src handles every input without crashing."
• "How is my Aristotle run going?"
• "What did Aristotle prove in my last project?"
• "Continue last week's project with the files I changed."

To send a whole folder, use an assistant that runs commands on your machine, such as Claude Code, Codex, Cursor, or VS Code. In a chat app, attach a few files instead.

Good to know

• Billing: your first run asks you to confirm which organization pays. Runs billed to it then start without asking for 90 days.
• Long runs: runs take minutes to days. Your assistant checks in for about 10 minutes, then stops. Ask again later, or follow the run in the web app.
• Questions: some runs ask you a question. Each question waits 15 minutes for your answer, then the run carries on without it.
• Uploads: up to 100 MB compressed. Credentials (.env files, keys, and .ssh folders) stay out, and so do .git folders, Lean's build outputs, and symbolic links. In a git checkout on macOS or Linux, files your .gitignore matches stay out too, unless git already tracks them. Elsewhere they're sent, and Aristotle drops those your top-level .gitignore matches once they arrive. To keep a file from being sent at all, move it out of the folder. Your assistant tells you what it left out. It names symbolic links only in a git checkout on macOS or Linux.
• Verilog: see Hardware verification for giving your assistant a design's top module, defines, and black boxes.

Tools

Your assistant picks these itself. They're listed here for reference.

• create_upload and start_run: send a project and start a run
• get_run and wait_for_run: check on a run
• answer_question: answer a run's question
• list_properties and get_property: read the results
• continue_run: start a finished project's next run
• list_projects and list_runs: find projects and their earlier runs
• create_download: download a project's files
• cancel_run: stop a run, asking you first about one started elsewhere

Use the CLI

Two commands, and Aristotle is verifying your code. The CLI needs Python 3.10 or later.

1

Install the CLI

On macOS or Linux, this installs uv if it is missing, installs the CLI, and logs you in:

curl -fsSL https://aristotle.harmonic.fun/install.sh | sh

Running it again upgrades. To install without logging in, give the variable to sh, not curl:

curl -fsSL https://aristotle.harmonic.fun/install.sh | ARISTOTLE_SKIP_LOGIN=1 sh

Or, on any system, Windows included:

uv tool install "aristotlelib>=3"

This installs aristotle globally, with no virtual environment to create or activate. It needs uv, a fast, reliable Python package manager.

2

Verify your code

aristotle submit "Hunt for real bugs with provable resolution" --project-dir ./my-project

If you are not logged in yet, the first run at a terminal offers to log you in: it shows a code to approve in your browser, and keeps the key for this machine. There is nothing to export. Aristotle works out the language from the files you upload, so there is nothing to declare either. It verifies Verilog and C.

The command prints a link to the project. Follow the run there, or pass --wait to stay in the terminal until it finishes. See Tracking properties for reading the result.

Other ways to install

Run Aristotle without installing it:

uvx --from "aristotlelib>=3" aristotle --help

Install into an existing virtual environment, which is also how you get the library:

pip install "aristotlelib>=3"

Upgrade regularly. New project management commands, clearer progress output, and safer upload behavior land often.

With uv:

uv tool upgrade aristotlelib

With pip:

pip install --upgrade aristotlelib

Logging in and out

aristotle login does on its own what the first submit offers to do. It prints the address of the approval page and a code, and opens the page when a browser is available. Sign in there, type the code, check that the page names your machine, and approve. Aristotle then makes a key named after the machine, and the CLI stores it in ~/.config/aristotle/credentials.json ($XDG_CONFIG_HOME/aristotle when that is set, %APPDATA%\aristotle on Windows), readable only by you. The key is listed in API keys, where you can revoke it.

aristotle logout removes the stored key. The key itself stays valid until you revoke it in API keys.

Scripts and CI

A build job has nobody to approve a login, so give it a key from API keys directly. The environment variable overrides a stored key, so a logged-in machine still behaves like the build agent when one is set:

export ARISTOTLE_API_KEY=your-api-key-here

Or pass a key to a single command, before or after the subcommand:

aristotle submit "My prompt" --api-key your-api-key-here

Verify your setup

aristotle --version

It prints aristotlelib 3. followed by the rest of the version, confirming the CLI is set up.