We introduce a

benchmark

that targets mathematical reasoning about real software logic, filling the gap between theorem proving and traditional software engineering tasks. The results reveal a fundamental limitation of LLM-only approaches: despite strong code understanding, they fail to reason exhaustively about program behavior, edge cases, and decision boundaries.

Using formally defined ground truth derived from automated state-space decomposition, the benchmark enables precise and reproducible evaluation of reasoning quality. Across all tested models, augmenting LLMs with formal reasoning via

CodeLogician closes a 41-47 percentage point accuracy gap

compared to LLM-only reasoning. These results show that formal reasoning is not merely an optimization, but a prerequisite for scalable and trustworthy AI-generated software.