ExVerus: Verus Proof Repair via Counterexample Reasoning
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
International Conference on Machine Learning | July 2026
Publications
-
-
-
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
-
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jay Lorch, Yuan Yao, Xiaoxing Ma
February 2026
-
-
-
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
-
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
-
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
-
-
-
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
-
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
-
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!
-
-
-
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
-
-
-
ExVerus: Verus Proof Repair via Counterexample Reasoning
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
International Conference on Machine Learning | July 2026
-
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jay Lorch, Yuan Yao, Xiaoxing Ma
February 2026
-
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
-
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
-
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
-
-
-
ExVerus: Verus Proof Repair via Counterexample Reasoning
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
International Conference on Machine Learning | July 2026
-
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
-
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jay Lorch, Yuan Yao, Xiaoxing Ma
February 2026
-
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
-
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
-
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
-
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
-
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
-
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
-
-
-
ExVerus: Verus Proof Repair via Counterexample Reasoning
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
International Conference on Machine Learning | July 2026
-
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
-
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jay Lorch, Yuan Yao, Xiaoxing Ma
February 2026
-
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
-
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
-
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
-
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
-
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
-
-
-
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!
-
-
-
ExVerus: Verus Proof Repair via Counterexample Reasoning
Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei
International Conference on Machine Learning | July 2026
-
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
-
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
-
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
-
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
-
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
-
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!
-
-
-
Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jay Lorch, Yuan Yao, Xiaoxing Ma
February 2026
-
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
-
-
-
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
-