# Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 58 references that are in the map.
- First posted on arXiv 14 Oct 2025.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Unit Test Case Generation with Transformers and Focal Context](https://mlsanity.com/paper/2009.05617/) (2020)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (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)
- [Pynguin: Automated Unit Test Generation for Python](https://mlsanity.com/paper/2202.05218/) (2022)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [Generating Accurate Assert Statements for Unit Test Cases using Pretrained Transformers](https://mlsanity.com/paper/2009.05634/) (2020)
- [TOGLL: Correct and Strong Test Oracle Generation with LLMs](https://mlsanity.com/paper/2405.03786/) (2024)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Doc2OracLL: Investigating the Impact of Documentation on LLM-based Test Oracle Generation](https://mlsanity.com/paper/2412.09360/) (2024)
- [AsserT5: Test Assertion Generation Using a Fine-Tuned Code Language Model](https://mlsanity.com/paper/2502.02708/) (2025)
- [ESBMC-Python: A Bounded Model Checker for Python Programs](https://mlsanity.com/paper/2407.03472/) (2024)
- [Breaking the Myth: Can Small Models Infer Postconditions Too?](https://mlsanity.com/paper/2507.10182/) (2025)

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

- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis](https://mlsanity.com/paper/2605.12694/) (2026)
- [Viverra: Text-to-Code with Guarantees](https://mlsanity.com/paper/2605.14972/) (2026)
- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)

## Abstract (arXiv)

Automatic software verifiers have become increasingly effective at the task of checking software against (formal) specifications. Yet, their adoption in practice has been hampered by the lack of such specifications in real world code. Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints embedded in code such as function names, comments or documentation. Using the generated postconditions as specifications in a subsequent verification, however, often leads verifiers to suggest invalid inputs, hinting at potential issues that ultimately turn out to be false alarms. To address this, we revisit the problem of specification inference from natural language in the context of automatic software verification. In the process, we introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts, consisting of postconditions as well as preconditions. We introduce metrics to validate and compare different NL2Contract approaches, using soundness, bug discriminative power of the generated contracts and their usability in the context of automatic software verification as key metrics. We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond. Our evaluation shows that (1) LLMs are generally effective at generating functional contracts sound for all possible inputs, (2) the generated contracts are sufficiently expressive for discriminating buggy from correct behavior, and (3) verifiers supplied with LLM inferred functional contracts produce fewer false alarms than when provided with postconditions alone. Further investigations show that LLM inferred preconditions generally align well with developers intentions which allows us to use automatic software verifiers to catch real-world bugs.