chiasmus 发布：给 LLM 接入 Z3、SWI-Prolog 形式化验证与 tree-sitter 代码分析的 MCP server

yogthos 在 GitHub 发布 chiasmus，一个让 LLM 通过 MCP 使用 Z3（SMT 求解器）、SWI-Prolog（含 library(clpfd)）和 tree-sitter 代码分析的 MCP server，npm 安装命令为 npm install -g chiasmus。它用模板流水线把自然语言问题转成形式化逻辑并给出数学意义上的验证结果，支持 RBAC 规则冲突检测、依赖约束求解、污点流追踪、死代码与影响分析等场景；chiasmus_graph 的可达类分析基于 O(V+E) 图算法，42 文件 TypeScript 仓库开启缓存后热命中约 2.5ms，对比冷解析约 170ms。