Click on "Install 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., "@Aare MCPverify this mortgage recommendation against compliance rules"
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.
aare-mcp
MCP (Model Context Protocol) server for aare-core Z3 SMT verification.
This server exposes aare-core's formal verification capabilities to LLM applications like Claude Desktop and Claude Code.
Installation
pip install aare-mcpOr install from source:
cd aare-mcp
pip install -e .Configuration
Claude Desktop
Add to your Claude Desktop configuration (~/Library/Application Support/Claude/claude_desktop_config.json on macOS):
{
"mcpServers": {
"aare-verify": {
"command": "aare-mcp"
}
}
}Claude Code
Add to your Claude Code MCP configuration:
{
"mcpServers": {
"aare-verify": {
"command": "aare-mcp"
}
}
}Available Tools
verify
Verify LLM output against a compliance ontology using Z3 SMT solver.
Parameters:
llm_output(string, required): The LLM-generated text to verifyontology(string, required): Name of the ontology to verify against
Example:
verify(
llm_output="Based on your income of $75,000 and the property value of $400,000, I recommend a loan amount of $320,000 with an APR of 6.5%.",
ontology="mortgage-compliance-v1"
)Response:
{
"verified": true,
"ontology": "mortgage-compliance-v1",
"violations": [],
"parsed_data": {
"income": 75000,
"property_value": 400000,
"loan_amount": 320000,
"apr": 6.5
},
"proof": {
"method": "Z3 SMT Solver",
"version": "4.12.1",
"results": []
},
"execution_time_ms": 12
}list_ontologies
List all available compliance ontologies.
Parameters: None
Response:
{
"ontologies": [
"example",
"hipaa-v1",
"mortgage-compliance-v1"
],
"count": 3
}parse_claims
Extract structured data from LLM output using ontology-defined extractors. Useful for debugging.
Parameters:
llm_output(string, required): The LLM-generated text to parseontology(string, required): Name of the ontology containing extractor definitions
Response:
{
"ontology": "mortgage-compliance-v1",
"parsed_data": {
"income": 75000,
"loan_amount": 320000
},
"extraction_details": {
"income": {
"value": 75000,
"confidence": 0.95,
"source": "75,000",
"extractor_type": "money"
}
}
}Custom Ontologies
Place custom ontology JSON files in the ontologies/ directory or set the ONTOLOGY_DIR environment variable:
export ONTOLOGY_DIR=/path/to/your/ontologies
aare-mcpDevelopment
# Install dev dependencies
pip install -e ".[dev]"
# Run tests
pytestLicense
MIT
This server cannot be installed
Resources
Unclaimed servers have limited discoverability.
Looking for Admin?
If you are the server author, to access and configure the admin panel.