Practical, High-Performance Verification in Rust

Publications

View by:

- VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
  
  Chuyue Sun, Yican Sun, Ethan Zhang, Daneshvar Amrollahi, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
  
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | April 2026
  
  Preprint
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
  
  December 2025
  
  Preprint Github
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github
- PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection
  
  Hayley LeBlanc, Jay Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, Vijay Chidambaram
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication
- Verus: A Practical Foundation for Systems Verification
  
  Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, Bryan Parno
  
  2024 Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication
- Automated Proof Generation for Rust Code via Self-Evolution
  
  Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
  
  ICLR 2025 | October 2024
  
  Publication
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github
- Verus: Verifying Rust Programs using Linear Ghost Types
  
  Andrea Lattuada, Travis Hance, Chanhee Cho, M. Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
  
  OOPSLA (in Proceedings of the ACM on Programming Languages) | March 2023
  
  Publication Author's Version

- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
  
  December 2025
  
  Preprint Github
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github
- Automated Proof Generation for Rust Code via Self-Evolution
  
  Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
  
  ICLR 2025 | October 2024
  
  Publication
- VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
  
  Chuyue Sun, Yican Sun, Ethan Zhang, Daneshvar Amrollahi, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
  
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | April 2026
  
  Preprint
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
  
  December 2025
  
  Preprint Github
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github
- PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection
  
  Hayley LeBlanc, Jay Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, Vijay Chidambaram
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication
- Verus: A Practical Foundation for Systems Verification
  
  Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, Bryan Parno
  
  2024 Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication
- Automated Proof Generation for Rust Code via Self-Evolution
  
  Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
  
  ICLR 2025 | October 2024
  
  Publication
- Verus: Verifying Rust Programs using Linear Ghost Types
  
  Andrea Lattuada, Travis Hance, Chanhee Cho, M. Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
  
  OOPSLA (in Proceedings of the ACM on Programming Languages) | March 2023
  
  Publication Author's Version
- VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
  
  Chuyue Sun, Yican Sun, Ethan Zhang, Daneshvar Amrollahi, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
  
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | April 2026
  
  Preprint
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
  
  December 2025
  
  Preprint Github
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github
- PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection
  
  Hayley LeBlanc, Jay Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, Vijay Chidambaram
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication
- Verus: A Practical Foundation for Systems Verification
  
  Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, Bryan Parno
  
  2024 Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication
- Automated Proof Generation for Rust Code via Self-Evolution
  
  Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
  
  ICLR 2025 | October 2024
  
  Publication
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github

- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
  
  December 2025
  
  Preprint Github
- VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
  
  Chuyue Sun, Yican Sun, Ethan Zhang, Daneshvar Amrollahi, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett
  
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | April 2026
  
  Preprint
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github
- PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection
  
  Hayley LeBlanc, Jay Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, Vijay Chidambaram
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication
- Verus: A Practical Foundation for Systems Verification
  
  Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, Bryan Parno
  
  2024 Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication
- Automated Proof Generation for Rust Code via Self-Evolution
  
  Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
  
  ICLR 2025 | October 2024
  
  Publication
- VeriSMo: A Verified Security Module for Confidential VMs
  
  Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
  
  OSDI 2024 | July 2024
  
  Jay Lepreau Best Paper Award
  
  Awarded Best Paper!
  
  Publication Github
- Verus: Verifying Rust Programs using Linear Ghost Types
  
  Andrea Lattuada, Travis Hance, Chanhee Cho, M. Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
  
  OOPSLA (in Proceedings of the ACM on Programming Languages) | March 2023
  
  Publication Author's Version

Practical, High-Performance Verification in Rust

Publications

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Automated Proof Generation for Rust Code via Self-Evolution

VeriSMo: A Verified Security Module for Confidential VMs

Verus: Verifying Rust Programs using Linear Ghost Types

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

Automated Proof Generation for Rust Code via Self-Evolution

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Automated Proof Generation for Rust Code via Self-Evolution

Verus: Verifying Rust Programs using Linear Ghost Types

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Automated Proof Generation for Rust Code via Self-Evolution

VeriSMo: A Verified Security Module for Confidential VMs

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Automated Proof Generation for Rust Code via Self-Evolution

VeriSMo: A Verified Security Module for Confidential VMs

Verus: Verifying Rust Programs using Linear Ghost Types