Generic Authenticated Data Structures, Formally. - Matthias Brun 002; Dmitriy Traytel (ITP, 2019)

Formalization of Generic Authenticated Data Structures. - Matthias Brun 002; Dmitriy Traytel (Arch. Formal Proofs, 2019)

Verified Progress Tracking for Timely Dataflow. - Matthias Brun 002; Sára Decova; Andrea Lattuada 001; Dmitriy Traytel (ITP, 2021)

Formalization of Timely Dataflow's Progress Tracking Protocol. - Matthias Brun 002; Sára Decova; Andrea Lattuada 001; Dmitriy Traytel (Arch. Formal Proofs, 2021)

Beyond isolation: OS verification as a foundation for correct applications. - Matthias Brun 002; Reto Achermann; Tej Chajed; Jon Howell; Gerd Zellweger; Andrea Lattuada 001 (HotOS, 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)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)