Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@MCP Server for Alloy Modeling Language create a model for a file system with users and permissions"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
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.
npm install
npm run buildRelated MCP server: OpenKer Modeler MCP Server
Run the server using stdio transport:
npm startOr use the built binary directly:
node build/index.js# Build TypeScript
npm run build
# Build and run
npm run dev
# Lint code
npm run lint
# Fix linting issues
npm run lint:fix
# Run tests
npm testexecute_alloy: Execute Alloy modeling language code and return structured JSON results
Input: code (string) - The Alloy code to execute
Output: JSON with instances, values, and solver results
alloy://docs: Basic Alloy language documentation and syntax reference
alloy://examples: Example Alloy models (graphs, file systems, state machines)
create_alloy_model: Generate an Alloy model based on a system description
Input: description (string) - Description of the system to model
sig Node {
edges: set Node
}
// No self-loops
fact { all n: Node | n not in n.edges }
// Find a graph with a cycle
run { some n: Node | n in n.^edges } for 5Execute Alloy modeling language code and return structured JSON results
Inputs: code (required).
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
Scored across 1 tool
With only one tool, there is no possibility of ambiguity or overlap between tools, making disambiguation perfect.
The single tool follows a clear verb_noun pattern (execute_alloy), and with no other tools, consistency is inherently perfect.
One tool is too few for a modeling language server, as it lacks essential operations like model validation, instance generation, or visualization, making the scope feel incomplete.
The tool surface is severely incomplete; it only allows code execution without supporting core Alloy workflows such as checking assertions, generating examples, or analyzing models, leading to significant gaps.
AI-native programming language and toolchain for accountable, verifiable agent-driven development.
Code intelligence platform for AI agents. 20 tools for architecture, security & impact analysis.
33 tools that make AI write, implement, and verify intent against explicit, testable constraints.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
