Giving LLMs a Formal Reasoning Engine for Code Analysis (yogthos.net) AI

The article describes Chiasmus, an MCP server that augments LLM code assistants with formal reasoning by parsing source code with tree-sitter, converting structure into Prolog facts, and using Tau Prolog (and Z3 for constraint solving) to answer questions like transitive reachability, dead code, cycles, and impact with proof-like certainty. It argues that this approach avoids the token-heavy, error-prone limitations of repeatedly “grepping” and reconstructing call chains via ad hoc search. It also notes the same architecture can verify properties of diagrams (e.g., Mermaid) and certain constraint problems beyond code.