Giving LLMs a Formal Reasoning Engine for Code Analysis

Chiasmus is an MCP server that combines large language models with formal reasoning engines (Z3 constraint solver and Tau Prolog) to improve code analysis. It addresses the fundamental limitation that LLMs struggle with exhaustive structural code analysis through ad hoc pattern matching. By parsing source files with tree-sitter and generating formal grammars, the system enables LLMs to answer complex code questions with certainty while consuming fewer tokens.