VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jay Lorch, Shan Lu
December 2025
Chris Hawblitzel
Senior Principal Researcher
Publications
-
-
-
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
-
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!
-
-
-
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno
Operating Systems Design and Implementation (OSDI) | July 2023
-
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
-
-
-
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel
OOPSLA (in Proceedings of the ACM on Programming Languages) | April 2022
Distinguished Paper Award
-
-
-
Storage Systems are Distributed Systems (So Verify Them That Way!)
Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno
Operating Systems Design and Implementation (OSDI) | November 2020
-
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
Verified Software: Theories, Tools, Experiments (VSTTE) | July 2020
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
-
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
-
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
-
-
Komodo: Using verification to disentangle secure-enclave hardware from software
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno
26th ACM Symposium on Operating Systems Principles | October 2017
-
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
-
IronFleet: Proving Safety and Liveness of Practical Distributed Systems
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Communications of the ACM | July 2017, Vol 60
CACM Research Highlight
-
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
-
-
-
IronFleet: Proving Practical Distributed Systems Correct
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
-
Automated and modular refinement reasoning for concurrent programs
Shaz Qadeer, Serdar Tasiran, Chris Hawblitzel
Computer Aided Verification (CAV) | July 2015
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
-
Automated and modular refinement reasoning for concurrent programs
Chris Hawblitzel, , Shaz Qadeer, Serdar Tasiran
MSR-TR-2015-8 | February 2015
-
-
-
Ironclad Apps: End-to-End Security via Automated Full-System Verification
Chris Hawblitzel, Jon Howell, Jay Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
-
Cosh: clear OS data sharing in an incoherent world
Andrew Baumann, Chris Hawblitzel, Kornilios Kourtis, Tim Harris, Timothy Roscoe
2014 Conference on Timely Results in Operating Systems (TRIOS '14) | October 2014
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
-
-
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
-
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
-
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
-
-
-
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
-
-
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
-
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
-
-
-
Inferable Object-Oriented Typed Assembly Language
Ross Tate, Juan Chen, Chris Hawblitzel
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI) | June 2010
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI)
-
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
Jean Yang, Chris Hawblitzel
PLDI | June 2010
Best Paper
-
-
-
Helios: Heterogeneous Multiprocessing with Satellite Kernels
Edmund B Nightingale, Orion Hodson, Ross McIlroy, Chris Hawblitzel, Galen Hunt
Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP '09) | October 2009
-
Automated Verification of Practical Garbage Collectors
POPL 09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2009
-
-
-
A Flexible Framework for Type Inference with Existential Quantification
Ross Tate, Juan Chen, Chris Hawblitzel
MSR-TR-2008-184 | December 2008
-
Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers
Jeremy Condit, Juan Chen, Chris Hawblitzel, Derrick Coetzee
ACM Conference on Programming Language Design and Implementation (PLDI 08) | June 2008
-
-
-
Checking the Hardware-Software Interface in Spec#
Kevin Bierhoff, Chris Hawblitzel
PLOS 07: 4th workshop on Programming languages and operating systems | October 2007
PLOS 07: 4th workshop on Programming languages and operating systems
-
Simple and Flexible Stack Types
Frances Perry, Chris Hawblitzel, Juan Chen
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 07) | July 2007
-
Sealing OS Processes to Improve Dependability and Safety
Galen Hunt, Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Bjarne Steensgaard, David Tarditi, Ted Wobber
Proceedings of the European Conference on Computer Systems (EuroSys) | March 2007
-
A Garbage-Collecting Typed Assembly Language
Chris Hawblitzel, Heng Huang, Lea Wittie, Juan Chen
MSR-TR-2006-169 | January 2007
ACM Workshop on Types in Language Design and Implementation (TLDI 07)
-
-
-
Deconstructing Process Isolation
Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Galen Hunt, Jim Larus
ACM SIGPLAN Workshop on Memory Systems Performance and Correctness | October 2006
-
Language Support for Fast and Reliable Message-based Communication in Singularity OS
Manuel Fahndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, Jim Larus, Steven Levi
Proceedings of the EuroSys 2006 Conference | April 2006
Best Paper
-
Sealing OS Processes to Improve Dependability and Security
Galen Hunt, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2006-51 | April 2006
-
-
-
An Overview of the Singularity Project
Galen Hunt, Jim Larus, Martin Abadi, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2005-135 | October 2005
-
Linear types for aliased resources
MSR-TR-2005-141 | October 2005
-
-
-
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
-
-
-
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
-
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
-
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel
OOPSLA (in Proceedings of the ACM on Programming Languages) | April 2022
Distinguished Paper Award
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
-
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
-
IronFleet: Proving Safety and Liveness of Practical Distributed Systems
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Communications of the ACM | July 2017, Vol 60
CACM Research Highlight
-
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
-
Automated and modular refinement reasoning for concurrent programs
Shaz Qadeer, Serdar Tasiran, Chris Hawblitzel
Computer Aided Verification (CAV) | July 2015
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
-
Automated and modular refinement reasoning for concurrent programs
Chris Hawblitzel, , Shaz Qadeer, Serdar Tasiran
MSR-TR-2015-8 | February 2015
-
Ironclad Apps: End-to-End Security via Automated Full-System Verification
Chris Hawblitzel, Jon Howell, Jay Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
-
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
-
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
-
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
-
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
-
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
Jean Yang, Chris Hawblitzel
PLDI | June 2010
Best Paper
-
Inferable Object-Oriented Typed Assembly Language
Ross Tate, Juan Chen, Chris Hawblitzel
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI) | June 2010
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI)
-
Automated Verification of Practical Garbage Collectors
POPL 09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2009
-
A Flexible Framework for Type Inference with Existential Quantification
Ross Tate, Juan Chen, Chris Hawblitzel
MSR-TR-2008-184 | December 2008
-
Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers
Jeremy Condit, Juan Chen, Chris Hawblitzel, Derrick Coetzee
ACM Conference on Programming Language Design and Implementation (PLDI 08) | June 2008
-
Checking the Hardware-Software Interface in Spec#
Kevin Bierhoff, Chris Hawblitzel
PLOS 07: 4th workshop on Programming languages and operating systems | October 2007
PLOS 07: 4th workshop on Programming languages and operating systems
-
Simple and Flexible Stack Types
Frances Perry, Chris Hawblitzel, Juan Chen
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 07) | July 2007
-
A Garbage-Collecting Typed Assembly Language
Chris Hawblitzel, Heng Huang, Lea Wittie, Juan Chen
MSR-TR-2006-169 | January 2007
ACM Workshop on Types in Language Design and Implementation (TLDI 07)
-
Language Support for Fast and Reliable Message-based Communication in Singularity OS
Manuel Fahndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, Jim Larus, Steven Levi
Proceedings of the EuroSys 2006 Conference | April 2006
Best Paper
-
-
-
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
-
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno
Operating Systems Design and Implementation (OSDI) | July 2023
-
Storage Systems are Distributed Systems (So Verify Them That Way!)
Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno
Operating Systems Design and Implementation (OSDI) | November 2020
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
Komodo: Using verification to disentangle secure-enclave hardware from software
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno
26th ACM Symposium on Operating Systems Principles | October 2017
-
IronFleet: Proving Safety and Liveness of Practical Distributed Systems
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Communications of the ACM | July 2017, Vol 60
CACM Research Highlight
-
IronFleet: Proving Practical Distributed Systems Correct
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
-
Ironclad Apps: End-to-End Security via Automated Full-System Verification
Chris Hawblitzel, Jon Howell, Jay Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
-
Cosh: clear OS data sharing in an incoherent world
Andrew Baumann, Chris Hawblitzel, Kornilios Kourtis, Tim Harris, Timothy Roscoe
2014 Conference on Timely Results in Operating Systems (TRIOS '14) | October 2014
-
Helios: Heterogeneous Multiprocessing with Satellite Kernels
Edmund B Nightingale, Orion Hodson, Ross McIlroy, Chris Hawblitzel, Galen Hunt
Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP '09) | October 2009
-
Sealing OS Processes to Improve Dependability and Safety
Galen Hunt, Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Bjarne Steensgaard, David Tarditi, Ted Wobber
Proceedings of the European Conference on Computer Systems (EuroSys) | March 2007
-
Deconstructing Process Isolation
Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Galen Hunt, Jim Larus
ACM SIGPLAN Workshop on Memory Systems Performance and Correctness | October 2006
-
Sealing OS Processes to Improve Dependability and Security
Galen Hunt, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2006-51 | April 2006
-
An Overview of the Singularity Project
Galen Hunt, Jim Larus, Martin Abadi, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2005-135 | October 2005
-
Linear types for aliased resources
MSR-TR-2005-141 | October 2005
-
-
-
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!
-
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
Verified Software: Theories, Tools, Experiments (VSTTE) | July 2020
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
-
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
-
IronFleet: Proving Practical Distributed Systems Correct
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
-
Ironclad Apps: End-to-End Security via Automated Full-System Verification
Chris Hawblitzel, Jon Howell, Jay Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
-
-
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
-
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
-
-
-
Linear types for aliased resources
MSR-TR-2005-141 | October 2005
-
-
-
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
-
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!
-
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno
Operating Systems Design and Implementation (OSDI) | July 2023
-
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel
OOPSLA (in Proceedings of the ACM on Programming Languages) | April 2022
Distinguished Paper Award
-
Storage Systems are Distributed Systems (So Verify Them That Way!)
Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno
Operating Systems Design and Implementation (OSDI) | November 2020
-
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
Verified Software: Theories, Tools, Experiments (VSTTE) | July 2020
-
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 | April 2019
-
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
Principles of Programming Languages (POPL 2019) | January 2019
-
Komodo: Using verification to disentangle secure-enclave hardware from software
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno
26th ACM Symposium on Operating Systems Principles | October 2017
-
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jay Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
Proceedings of the USENIX Security Symposium | August 2017
Distinguished Paper Award
-
Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
-
IronFleet: Proving Practical Distributed Systems Correct
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
-
Automated and modular refinement reasoning for concurrent programs
Shaz Qadeer, Serdar Tasiran, Chris Hawblitzel
Computer Aided Verification (CAV) | July 2015
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
-
Ironclad Apps: End-to-End Security via Automated Full-System Verification
Chris Hawblitzel, Jon Howell, Jay Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
-
Cosh: clear OS data sharing in an incoherent world
Andrew Baumann, Chris Hawblitzel, Kornilios Kourtis, Tim Harris, Timothy Roscoe
2014 Conference on Timely Results in Operating Systems (TRIOS '14) | October 2014
-
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
-
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
-
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
-
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
Jean Yang, Chris Hawblitzel
PLDI | June 2010
Best Paper
-
Inferable Object-Oriented Typed Assembly Language
Ross Tate, Juan Chen, Chris Hawblitzel
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI) | June 2010
ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI)
-
Helios: Heterogeneous Multiprocessing with Satellite Kernels
Edmund B Nightingale, Orion Hodson, Ross McIlroy, Chris Hawblitzel, Galen Hunt
Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP '09) | October 2009
-
Automated Verification of Practical Garbage Collectors
POPL 09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2009
-
Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers
Jeremy Condit, Juan Chen, Chris Hawblitzel, Derrick Coetzee
ACM Conference on Programming Language Design and Implementation (PLDI 08) | June 2008
-
Checking the Hardware-Software Interface in Spec#
Kevin Bierhoff, Chris Hawblitzel
PLOS 07: 4th workshop on Programming languages and operating systems | October 2007
PLOS 07: 4th workshop on Programming languages and operating systems
-
Simple and Flexible Stack Types
Frances Perry, Chris Hawblitzel, Juan Chen
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 07) | July 2007
-
Sealing OS Processes to Improve Dependability and Safety
Galen Hunt, Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Bjarne Steensgaard, David Tarditi, Ted Wobber
Proceedings of the European Conference on Computer Systems (EuroSys) | March 2007
-
Deconstructing Process Isolation
Mark Aiken, Manuel Fahndrich, Chris Hawblitzel, Galen Hunt, Jim Larus
ACM SIGPLAN Workshop on Memory Systems Performance and Correctness | October 2006
-
Language Support for Fast and Reliable Message-based Communication in Singularity OS
Manuel Fahndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, Jim Larus, Steven Levi
Proceedings of the EuroSys 2006 Conference | April 2006
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
-
IronFleet: Proving Safety and Liveness of Practical Distributed Systems
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
Communications of the ACM | July 2017, Vol 60
CACM Research Highlight
-
-
-
Automated and modular refinement reasoning for concurrent programs
Chris Hawblitzel, , Shaz Qadeer, Serdar Tasiran
MSR-TR-2015-8 | February 2015
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
-
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
-
A Flexible Framework for Type Inference with Existential Quantification
Ross Tate, Juan Chen, Chris Hawblitzel
MSR-TR-2008-184 | December 2008
-
A Garbage-Collecting Typed Assembly Language
Chris Hawblitzel, Heng Huang, Lea Wittie, Juan Chen
MSR-TR-2006-169 | January 2007
ACM Workshop on Types in Language Design and Implementation (TLDI 07)
-
Sealing OS Processes to Improve Dependability and Security
Galen Hunt, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Jim Larus, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2006-51 | April 2006
-
An Overview of the Singularity Project
Galen Hunt, Jim Larus, Martin Abadi, Mark Aiken, Paul Barham, Manuel Fahndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, Brian Zill
MSR-TR-2005-135 | October 2005
-
Linear types for aliased resources
MSR-TR-2005-141 | October 2005
-