A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. - Antoine Delignat-Lavaud; Cédric Fournet; Bryan Parno; Jonathan Protzenko; Tahina Ramananandro; Jay Bosamiya; Joseph Lallemand; Itsaka Rakotonirina; Yi Zhou 025 (IACR Cryptol. ePrint Arch., 2020)

Linear types for large-scale systems verification. - Jialin Li 001; Andrea Lattuada 001; Yi Zhou 025; Jonathan Cameron; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2022)

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares. - Yi Zhou 025; Sydney Gibson; Sarah Cai; Menucha Winchell; Bryan Parno (CCS, 2023)

Mariposa: Measuring SMT Instability in Automated Program Verification. - Yi Zhou 025; Jay Bosamiya; Yoshiki Takashima; Jessica Li; Marijn Heule; Bryan Parno (FMCAD, 2023)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

A Framework for Debugging Automated Program Verification Proofs via Proof Actions. - Chanhee Cho; Yi Zhou 025; Jay Bosamiya; Bryan Parno (CAV (1), 2024)

Context Pruning for More Robust SMT-based Program Verification. - Yi Zhou 025; Jay Bosamiya; Jessica Li; Marijn J. H. Heule; Bryan Parno (FMCAD, 2024)

Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. - Yi Zhou 025; Amar Shah; Zhengyao Lin; Marijn Heule; Bryan Parno (CADE, 2025)