Constraint Validator MCP
Relevant source files
The following files were used as context for generating this wiki page:
The Constraint Validator MCP is a specialized Model Context Protocol server designed to validate logical consistency within complex datasets and rules. It utilizes the Z3 SMT (Satisfiability Modulo Theories) solver to detect contradictions, provide logical explanations for conflicts, and check consistency across various entities.
Integrated into the Engineering Platform's suite of domain-agnostic tools, it serves critical functions in identifying business rule conflicts, validating data migrations, and detecting contradictions in project requirements. It operates alongside other research engines like the research-swarm and basin-analyzer to ensure high-fidelity, logically sound AI outputs.
Sources: mcp-servers/README.md:126-133, README.md:118-121, mcp-servers/constraint-validator/server.py:1-12
Architecture and Data Flow
The system follows a pipeline that transitions from natural language findings to formal logical constraints, which are then processed by a mathematical solver.
System Workflow
- Extraction: Natural language findings are converted into formal logic using LLM-assisted extraction.
- Validation: Formal logic forms are passed to the Z3 SMT solver to check for satisfiability (SAT).
- Analysis: If constraints are unsatisfiable (UNSAT), the server identifies the "UNSAT core"—the specific subset of rules that cause the contradiction.
- Resolution: Constraints are ranked by legal or organizational authority to suggest which rules should take precedence during conflict resolution.
The diagram above illustrates the logical flow from unstructured input to resolved constraints.
Sources: mcp-servers/constraint-validator/server.py:53-118, mcp-servers/README.md:126-140
Core Components
The server is built around three primary logic modules that handle the lifecycle of a constraint.
Constraint Extractor
This component uses an LLM (integrated via LiteLLM) to parse investigation findings. It extracts "logic forms" and maintains "provenance"—tracking exactly which document, page, or quote a specific rule originated from.
Z3 Validator
The core engine utilizing the Z3 theorem prover. It performs the mathematical check to see if a set of constraints can all be true simultaneously. It supports both "hard" constraints (must be true) and "soft" constraints (preferred but can be violated).
Authority Ranker
A specialized module that applies a hierarchy (e.g., Supreme Court > Circuit > District) to resolve conflicts. When Z3 detects an UNSAT core, the Authority Ranker determines which constraint carries more weight.
Sources: mcp-servers/constraint-validator/server.py:30-45, mcp-servers/constraint-validator/server.py:102-118
MCP Tool Definitions
The server exposes several tools through the MCP protocol, allowing AI agents to interact with the validation logic.
| Tool Name | Purpose | Key Inputs |
|---|---|---|
extract_constraints | Converts findings to formal logic. | Findings (quotes, docs, significance) |
validate_consistency | Runs the Z3 SMT solver check. | Array of constraint objects |
explain_conflict | Maps UNSAT cores to source docs. | UNSAT core IDs, original constraints |
rank_by_authority | Ranks rules by hierarchy level. | Constraints with source provenance |
Sources: mcp-servers/constraint-validator/server.py:53-118
Validation Logic Implementation
The validation process converts JSON-based constraint definitions back into internal Constraint objects before passing them to the solver.
# From mcp-servers/constraint-validator/server.py:167-185
c = Constraint(
id=cd.get('id', f'c_{len(constraint_objects)}'),
constraint_type=ConstraintType(cd.get('constraint_type', 'assertion')),
subject=cd.get('subject', ''),
predicate=cd.get('predicate'),
variables=cd.get('variables', []),
logic_form=cd.get('logic_form', ''),
natural_language=cd.get('natural_language', ''),
confidence=cd.get('confidence', 0.8),
provenance=prov,
is_hard=cd.get('is_hard', True)
)
Sources: mcp-servers/constraint-validator/server.py:167-185
Server Configuration
The server operates on a Python-based stack using aiohttp for the transport layer, supporting both HTTP and SSE (Server-Sent Events).
| Environment Variable | Description | Default Value |
|---|---|---|
MCP_SERVER_PORT | Port for the MCP server. | 9385 |
LITELLM_URL | Endpoint for the LLM extraction. | http://litellm:4000 |
LITELLM_API_KEY | API key for LiteLLM access. | sk-1234 |
MCP_AUTH_TOKEN | Token for securing the server. | "" |
Sources: mcp-servers/constraint-validator/server.py:21-25
Sequence of Conflict Resolution
When a conflict is detected, the server follows a specific sequence to provide a human-readable explanation and a path to resolution.
This sequence demonstrates the interaction between the Z3 mathematical results and the legal authority logic.
Sources: mcp-servers/constraint-validator/server.py:190-230, mcp-servers/constraint-validator/server.py:313-335
Conclusion
The Constraint Validator MCP provides a robust mathematical foundation for AI agents to ensure their reasoning remains logically consistent. By combining the Z3 SMT solver with domain-specific authority models and provenance tracking, it bridges the gap between unstructured natural language and verifiable logical systems. Its primary significance lies in its ability to not only detect that a conflict exists but also to explain why it exists and provide a hierarchical basis for resolving it.