chiasmus

Chiasmus 是一个面向大语言模型（LLM）的 MCP 服务器，为 AI 助手提供形式化验证能力。它集成 Z3 SMT 求解器与 SWI-Prolog（含 CLP(FD)），支持将自然语言问题转化为逻辑约束并进行数学级验证；同时基于 tree-sitter 实现源码解析，结合 Prolog 进行调用图分析，完成可达性、污点传播、死代码识别与影响分析等任务。适用于安全敏感场景下的权限策略验证、依赖兼容性求解、前后端校验一致性检查、工作流状态建模及自动化代码审查等需要可证明结论的工程实践。