alloy-analyzer-mcp

An MCP server that executes Alloy specifications and returns validation results as JSON.

Requirements

• Node.js >= 18
• Java >= 17 (required to run the Alloy JAR)

Setup

npm install

Development Commands

npm run dev        # Development mode (tsx watch)
npm run build      # TypeScript build
npm test           # Run tests
npm run pack:check # Check package contents

MCP Client Configuration

Local build:

{
  "mcpServers": {
    "alloy": {
      "command": "node",
      "args": ["/absolute/path/to/alloy-analyzer-mcp/build/index.js"]
    }
  }
}

Via npx:

{
  "mcpServers": {
    "alloy": {
      "command": "npx",
      "args": ["-y", "alloy-analyzer-mcp"]
    }
  }
}

Tool

execute_alloy

Executes an Alloy specification and returns the validation result as JSON.

Parameters:

| Name | Type | Description | |------|------|------| | code | string (required) | Source code for the Alloy specification |

Example Alloy specification:

sig Person {
  friends: set Person
}

fact noSelfFriend {
  no p: Person | p in p.friends
}

check symmetry {
  all p, q: Person | p in q.friends implies q in p.friends
} for 5

Example successful response:

{
  "duration": 123,
  "incremental": false,
  "instances": [
    {
      "messages": [],
      "skolems": {},
      "state": 0,
      "values": {}
    }
  ],
  "localtime": "2025-01-01T00:00:00",
  "loopstate": -1,
  "sigs": {},
  "timezone": "Asia/Tokyo",
  "utctime": 1700000000000
}

Example error response:

{
  "error": "Syntax error at line 3, column 1: ..."
}

License

MIT