MCP Server for Alloy Modeling Language
This is an MCP server that can let you run a local Alloy-Language server. You can use it to allow an LLM-powered agent to generate and execute Alloy modeling code.
Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks. This site provides language documentation, tool downloads, and a repository of links to case studies and applications. As the open source community grows, this site will also provide access to extensions of the Alloy Analyzer, and tools built on top of it and on top of Kodkod, its model finding engine. (alloytools.org)
This MCP server uses the alloy-lang npm package which bundles the language binary for easy use from nodejs.
Installation
Usage
As an MCP Server
Run the server using stdio transport:
Or use the built binary directly:
Development
MCP Features
Tools
execute_alloy: Execute Alloy modeling language code and return structured JSON results
Input:
code(string) - The Alloy code to executeOutput: JSON with instances, values, and solver results
Resources
alloy://docs: Basic Alloy language documentation and syntax reference
alloy://examples: Example Alloy models (graphs, file systems, state machines)
Prompts
create_alloy_model: Generate an Alloy model based on a system description
Input:
description(string) - Description of the system to model
Example Alloy Code
Resources
local-only server
The server can only run on the client's local machine because it depends on local resources.
Tools
Enables LLM-powered agents to generate, execute, and analyze Alloy modeling language code for software modeling and formal verification. Provides tools to run Alloy models, access documentation and examples, and generate models from system descriptions.