Verus (proof system)
 | The topic of this article may not meet Wikipedia's general notability guideline. (September 2026) |
Verus is a formal verification tool for the Rust programming language that uses SMT solvers in its implementation.[1]
Verus has been used by Amazon Web Services and Microsoft for provably correct software development.[2][3] The AutoVerus system uses large language models to construct Verus proofs for Rust programs.[4]
References
[edit]- ↑ Lattuada, Andrea; Hance, Travis; Cho, Chanhee; Brun, Matthias; Subasinghe, Isitha; Zhou, Yi; Howell, Jon; Parno, Bryan; Hawblitzel, Chris (2023-04-06). "Verus: Verifying Rust Programs using Linear Ghost Types". Proceedings of the ACM on Programming Languages. 7 (OOPSLA1). New York, NY, USA: Association for Computing Machinery: 85:286–85:315. doi:10.1145/3586037.
- ↑ Parno, Bryan (2026-08-31). "Developing provably correct Rust code with Verus". Amazon Science. Retrieved 2026-09-17.
- ↑ "Practical System Verification". Microsoft Research. Retrieved 2026-09-17.
- ↑ Yang, Chenyuan; Li, Xuheng; Misu, Md Rakib Hossain; Yao, Jianan; Cui, Weidong; Gong, Yeyun; Hawblitzel, Chris; Lahiri, Shuvendu; Lorch, Jacob R.; Lu, Shuai; Yang, Fan; Zhou, Ziqiao; Lu, Shan (2025-10-09). "AutoVerus: Automated Proof Generation for Rust Code". Proceedings of the ACM on Programming Languages. 9 (OOPSLA2): 3454–3482. doi:10.1145/3763174. ISSN 2475-1421.
External links
[edit]
| Compilers | |
|---|---|
| Package management, build tools | |
| Development tools | |
| Libraries, frameworks | |
| Verification | |
| Embedded, real-time | |
| Related topics | |
 | This computer science article is a stub. You can help Wikipedia by adding missing information. |