VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911595023564800 |
|---|---|
| author | Yang, Chenyuan Neamtu, Natalie Hawblitzel, Chris Lorch, Jacob R. Lu, Shan |
| author_facet | Yang, Chenyuan Neamtu, Natalie Hawblitzel, Chris Lorch, Jacob R. Lu, Shan |
| contents | Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_18436 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | VeruSAGE: A Study of Agent-Based Verification for Rust Systems Yang, Chenyuan Neamtu, Natalie Hawblitzel, Chris Lorch, Jacob R. Lu, Shan Operating Systems Artificial Intelligence Formal Languages and Automata Theory Software Engineering Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software. |
| title | VeruSAGE: A Study of Agent-Based Verification for Rust Systems |
| topic | Operating Systems Artificial Intelligence Formal Languages and Automata Theory Software Engineering |
| url | https://arxiv.org/abs/2512.18436 |