{"id":1097610,"date":"2024-10-25T14:55:19","date_gmt":"2024-10-25T21:55:19","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&p=1097610"},"modified":"2025-12-23T11:58:56","modified_gmt":"2025-12-23T19:58:56","slug":"practical-system-verification","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/practical-system-verification\/","title":{"rendered":"Practical System Verification"},"content":{"rendered":"
\n\t
\n\t\t
\n\t\t\t\t\t<\/div>\n\t\t\n\t\t
\n\t\t\t\n\t\t\t
\n\t\t\t\t\n\t\t\t\t
\n\t\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\n\n

Practical, High-Performance Verification in Rust<\/h1>\n\n\n\n

<\/p>\n\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/div>\n<\/section>\n\n\n\n\n\n

Formal verification is a promising approach to eliminate bugs at compile time, before software ships. Unfortunately, verifying the correctness of system software traditionally requires heroic developer effort. In this project, we aim to enable accessible, faster, cheaper verification of rich properties for realistic systems written in Rust using Verus. Verus is an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, with no need to learn a new language. At the same time, Verus takes advantage of Rust\u2019s linear types and borrow checking to express ownership and separation in proofs. We are using Verus to develop high-performance, verifiably correct systems. We are also exploring the use of Large Language Models to further ease the effort of developing proof with Verus.<\/p>\n\n\n\n

The Verus repository can be found at https:\/\/github.com\/verus-lang\/verus (opens in new tab)<\/span><\/a> .<\/p>\n\n\n\n

Our LLM-for-Verus repository, including our Verus proof synthesis benchmark suites (Verus-Bench & VeruSAGE-Bench), can be found at microsoft\/verus-proof-synthesis (opens in new tab)<\/span><\/a><\/p>\n\n\n\n\n\n

<\/p>\n","protected":false},"excerpt":{"rendered":"

Formal verification is a promising approach to eliminate bugs at compile time, before software ships. Unfortunately, verifying the correctness of system software traditionally requires heroic developer effort. In this project, we aim to enable accessible, faster, cheaper verification of rich properties for realistic systems written in Rust using Verus. Verus is an SMT-based tool for formally […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560,13547],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-1097610","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-research-area-systems-and-networking","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2023-01-01","related-publications":[1034709,1034787,1083954,1097751,1097760,1139493,1159286,1159305,1161796],"related-downloads":[],"related-videos":[],"related-groups":[144927,1021704],"related-events":[],"related-opportunities":[],"related-posts":[1099821,1122786],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Chris Hawblitzel","user_id":31425,"people_section":"Related people","alias":"chrishaw"},{"type":"user_nicename","display_name":"Jay Lorch","user_id":32732,"people_section":"Related people","alias":"lorch"},{"type":"user_nicename","display_name":"Shan Lu","user_id":43215,"people_section":"Related people","alias":"shanlu"},{"type":"user_nicename","display_name":"Ziqiao Zhou","user_id":40390,"people_section":"Related people","alias":"ziqiaozhou"},{"type":"guest","display_name":"Chenyuan Yang","user_id":1159338,"people_section":"Related people","alias":""},{"type":"guest","display_name":"Xuheng Li","user_id":1159339,"people_section":"Related people","alias":""},{"type":"guest","display_name":"Natalie Neamtu","user_id":1159342,"people_section":"Related people","alias":""},{"type":"guest","display_name":"Md Rakib Hossain","user_id":1159347,"people_section":"Related people","alias":""},{"type":"guest","display_name":"Jianan Yao","user_id":1159349,"people_section":"Related people","alias":""},{"type":"user_nicename","display_name":"Peng Cheng","user_id":33225,"people_section":"Related people","alias":"pengc"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/1097610","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":10,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/1097610\/revisions"}],"predecessor-version":[{"id":1159365,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/1097610\/revisions\/1159365"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1097610"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1097610"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1097610"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1097610"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=1097610"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}