Alloy MCP Server

A local Model Context Protocol (MCP) server that provides a headless bridge between Claude Desktop (or Roo Code) and the Alloy Analyzer (Kodkod SAT solver). This allows AI agents to write, compile, and execute formal verification models and read the raw mathematical graph structures directly back into their context window.

Features

• Fast Syntax Checking: Validates Alloy grammar using file paths without booting the heavy SAT solver.

• Asynchronous Execution & Timeouts: Handles highly complex models that take minutes or hours to solve. The server safely detaches background tasks to prevent LLM tool timeouts.

• Context Window Protection: Automatically archives all discovered counterexamples locally to all_counterexamples.txt, but only returns the first 5 to the LLM to prevent token bloat.

• Alloy 6 Temporal Support: Natively unpacks and formats behavioral traces (var signatures) step-by-step so the LLM can easily read state mutations over time.

Related MCP server: mcp-server-quint

Prerequisites

To run this server locally, you must have the following installed:

• Node.js (v18 or higher)

• Java Development Kit (JDK) (v11 or higher)

• Claude Desktop App (or Roo Code inside VS Code)

Installation & Setup

1. Clone the repository:

   git clone https://github.com/joel6603/alloy-mcp-server.git
   cd alloy-mcp-server

2. Install Node dependencies:

   npm install

3. Download the Alloy Engine:

   • Download the official Alloy 6 .jar file from AlloyTools.

   • Rename the file to org.alloytools.alloy.dist.jar.

   • Place it directly in the root folder of this project.

4. Compile the Java Backend:

   # On Windows:
   javac -cp "org.alloytools.alloy.dist.jar;." RunAlloy.java
   
   # On Mac/Linux:
   javac -cp "org.alloytools.alloy.dist.jar:." RunAlloy.java

Connecting to Claude Desktop

Locate your Claude Desktop configuration file:

• Windows: %APPDATA%\Claude\claude_desktop_config.json

• Mac: ~/Library/Application Support/Claude/claude_desktop_config.json

Add the server to your configuration, ensuring the absolute path points to where you cloned this repository:

{
  "mcpServers": {
    "alloy": {
      "command": "node",
      "args": [
        "D:/path/to/your/repo/alloy-mcp-server/index.js"
      ]
    }
  }
}

Note: Restart Claude Desktop completely after saving this file.

Available MCP Tools

• check_alloy_syntax

  • Input: filename (Absolute path to the .als file).

  • Description: Reads the file directly from the hard drive and instantly returns line/column syntax errors without triggering the Kodkod solver.

• run_alloy_model

  • Input: filename (Absolute path) and an optional commandName (defaults to "all").

  • Description: Executes the SAT solver.

    • If execution is fast, it returns a maximum of 5 formatted counterexamples to the chat.

    • If execution exceeds 45 seconds, it returns a safe "Background Execution Started" message to the AI while continuing to run silently.

    • In all cases, every discovered solution (up to 200) is saved to all_counterexamples.txt in the server root for manual review.