# Teaching Code LLMs to Reason with Intermediate Formal Specifications

arXiv: https://arxiv.org/abs/2607.04232 · HTML: https://mlsanity.com/paper/2607.04232/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 14 of its 46 references that are in the map.
- First posted on arXiv 5 Jul 2026.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 14 of 14)

- [Unit Test Case Generation with Transformers and Focal Context](https://mlsanity.com/paper/2009.05617/) (2020)
- [SpecRover: Code Intent Extraction via LLMs](https://mlsanity.com/paper/2408.02232/) (2024)
- [TOGA: A Neural Method for Test Oracle Generation](https://mlsanity.com/paper/2109.09262/) (2021)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [CoverUp: Effective High Coverage Test Generation for Python](https://mlsanity.com/paper/2403.16218/) (2024)
- [Can Large Language Models Write Good Property-Based Tests?](https://mlsanity.com/paper/2307.04346/) (2023)
- [Generating Accurate Assert Statements for Unit Test Cases using Pretrained Transformers](https://mlsanity.com/paper/2009.05634/) (2020)
- [Using Transfer Learning for Code-Related Tasks](https://mlsanity.com/paper/2206.08574/) (2022)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [Toward Trustworthy Neural Program Synthesis](https://mlsanity.com/paper/2210.00848/) (2022)
- [HoarePrompt: Structural Reasoning About Program Correctness in Natural Language](https://mlsanity.com/paper/2503.19599/) (2025)
- [EvoSpex: An Evolutionary Algorithm for Learning Postconditions](https://mlsanity.com/paper/2102.13569/) (2021)
- [SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference](https://mlsanity.com/paper/2602.20610/) (2026)

## Built on by (most cited first, 1 of 1)

- [Rules to Tools: Executable Checks for LLM Agents in Scientific Computing](https://mlsanity.com/paper/2610.00313/) (2026)

## Abstract (arXiv)

Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.