Can structured templates replace formal verification for code reasoning?

Code-reasoning approaches have historically clustered at two extremes. At one end, unstructured CoT: prompt the model to reason about the code freely. The output is in natural language, the reasoning is opaque to verification, and the model can claim conclusions without justifying them. At the other end, full formal verification: translate the code (or the reasoning) into a formal language like Lean or Coq and use automated proof checkers. The output is rigorous, but fully formalizing language semantics for arbitrary repository code spanning multiple frameworks is impractical.

The Agentic Code Reasoning paper argues both extremes are suboptimal for production code agents, and identifies the middle ground: semi-formal reasoning. Stay in natural language, but require structured templates that enforce the discipline formal verification provides. The agent fills in a function trace table (every function examined, with file:line locations and verified behavior), a data flow analysis (how key variables move through the code), semantic properties with explicit evidence, and an alternative-hypothesis check.

The template requirements do work that formalization would otherwise have to do. They prevent the model from skipping cases — the table demands every relevant function be examined. They prevent unsupported claims — each semantic property must come with line-anchored evidence. They prevent confirmation bias — the alternative-hypothesis check forces consideration of why the conclusion might be wrong.

The deeper design principle: completeness scaffolding can substitute for formalism. The reliability gains from formal methods come partly from the rigor of the formalism and partly from the forced discipline of writing everything out. Templates capture the second contribution without paying the cost of the first. The agent reasons in natural language, which works across all the languages and frameworks in a real codebase, but the structure of the reasoning is enforced enough to function as a verification certificate.

The pattern generalizes. Wherever full formalization is impractical but unstructured reasoning is unreliable, structured natural-language templates may bridge the gap.