Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.11315 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916003356606464 |
|---|---|
| author | Li, Zhaorui Song, Chengyu |
| author_facet | Li, Zhaorui Song, Chengyu |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_11315 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Natural Language based Specification and Verification Li, Zhaorui Song, Chengyu Software Engineering Artificial Intelligence Cryptography and Security 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. |
| title | Natural Language based Specification and Verification |
| topic | Software Engineering Artificial Intelligence Cryptography and Security |
| url | https://arxiv.org/abs/2605.11315 |