CSL-Core is a policy engine that formally verifies AI agent constraints using Z3. Instead of prompting an LLM to behave, you write a small policy in CSL (Constitutional Specification Language), Z3 proves it has no contradictions at compile time, and a deterministic runtime enforces it — completely outside the model.
We just shipped a built-in MCP server with 4 tools: verify_policy: Z3 formal verification in one call simulate_policy: test any JSON input, get ALLOWED/BLOCKED explain_policy: human-readable breakdown of any policy scaffold_policy: describe what you want in English, get a CSL template This means you can do this from Claude Desktop or Cursor: "Write me a policy that blocks transfers over $5000 for non-admin users" → scaffold generates a CSL template → verify proves it has no contradictions → simulate tests your edge cases → all without leaving your editor The full loop: From English description to mathematically verified, runtime-enforced policy; happens inside your AI assistant. Why not just prompt the LLM to enforce rules? We benchmarked GPT-4o, Claude Sonnet 4, and Gemini 2.0 Flash as guardrails with a hardened system prompt. Every model was bypassed by at least one attack (context spoofing, multi-turn role escalation, unicode homoglyphs). CSL-Core blocked all of them; because the LLM never touches the enforcement layer. Setup: pip install "csl-core[mcp]" Claude Desktop config: { "mcpServers": { "csl-core": { "command": "csl-core-mcp" } } } Or with Docker: docker build -t csl-core-mcp . docker run -i csl-core-mcp GitHub: https://github.com/Chimera-Protocol/csl-core Listed on awesome-mcp-servers: https://github.com/punkpeye/awesome-mcp-servers Previous Show HN discussion: https://news.ycombinator.com/item?id=46963250 Would love feedback, especially from anyone building agentic systems where safety guarantees matter. |