Beyond postconditions: Can large language models infer formal contracts for automatic software verification?

Note

NL2Contract: LLMs infer full functional contracts; verifiers using these detect genuine bugs in real-world code.