Natural Language based Specification and Verification
It addresses the challenge of making formal verification accessible for LLM-generated code by replacing rigid formal specifications with natural language.
The paper explores using LLMs to generate and verify specifications in natural language for preventing vulnerable code, showing promising preliminary results.
Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal is to prevent such models from producing vulnerable implementations in the first place. Formal verification offers a principled route to this objective, but existing verification pipelines typically require specifications written in rigid formal languages. Prior work has explored using LLMs to synthesize such specifications, with limited success. In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language. Our preliminary results suggest that this approach is promising.