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

TL;DR

The paper tackles the challenge of deriving formal specifications from natural language to support automatic software verification. It introduces NL2Contract, a task that uses LLMs to infer functional contracts comprising preconditions and postconditions from developer intent, validated via verification soundness and sufficient completeness. Through experiments on HumanEval$^+$ and Python-by-Contract, NL2Contract demonstrates that LLMs can generate sound, bug-discriminating contracts that improve real-bug detection with automatic verifiers and substantially reduce false alarms compared to postcondition-only approaches. The work also formalizes evaluation metrics, presents an exception-based contract encoding for Python, and shows that inferred preconditions align well with developer intent, enabling practical bug catching. Overall, NL2Contract offers a viable path to harness natural-language hints for robust, verifier-friendly specifications in real-world software.

Abstract

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.

Figures (8)

• Figure 1: Example task for NL2Contract. The goal is to translate informal natural language descriptions into functional contracts which can be automatically checked by existing software verifiers.
• Figure 2: Overview of NL2Contract's specification validation process.
• Figure 3: Prompt template for generating functional contracts from natural language descriptions. Dark gray parts are automatically filled in during prompt construction. Violet parts are inferred by the LLM from the given context.
• Figure 4: Comparison of LLMs under different prompts. Left (a) shows the percentage of specifications that are unsound due to violations of reference precondition. Right (b) shows $sound@1$ of the postconditions.
• Figure 5: Comparison of LLMs under different prompts with respect to postcondition completeness.