chiasmus

Chiasmus 是一个MCP服务器，它为语言模型提供了形式化验证的能力。该项目利用Z3（SMT求解器）和SWI-Prolog（通过`prolog-wasm-full`支持`library(clpfd)`），结合基于tree-sitter的源代码分析技术，将自然语言问题转化为形式逻辑，并以数学上的确定性验证结果，同时提供调用图分析功能来检测可达性、死代码及影响分析等。适用于需要确保软件系统安全性、一致性和优化性的场景，如RBAC规则冲突检查、依赖包版本兼容性分析、用户输入数据流追踪、前后端验证一致性测试以及工作流程状态分析等。项目采用TypeScript编写，遵循Apache License 2.0开源许可协议。