Federico Poli

Hi! I’m a protocol engineer at delta Network in Zurich, where my work ranges from design to implementation, testing, and deployment of consensus-based network nodes. I enjoy applying semi-formal methods to test the correctness of real-world components, as it usually strikes a good balance between maintenance and testing guarantees. Broadly speaking, my interests revolve around Rust, distributed systems, automated reasoning, and machine learning.

In 2024, I completed my PhD in Computer Science at ETH Zurich, where I conducted research in the Programming Methodology Group in collaboration with Peter Müller (my main advisor) and Alexander J. Summers. My doctoral work focused on automated reasoning applied to the Rust language, creating tools to detect bugs and ensure software correctness. This involved extensive work in software verification, static analysis, compilers, and Rust language semantics. Notably, I am a co-creator of Prusti, an automated verifier for Rust software that we began developing in 2017.

My professional experience includes internships at AWS, where I worked on automated reasoning, at Google, where I focused on self-supervised machine learning, and at CERN, where I worked with Python and information retrieval.

Contacts:

• Email
• GitHub
• Google Scholar
• LinkedIn

PhD work

Projects

• Prusti — Our automated verifier for Rust. I worked on this from 2017 to 2024.
• Prusti Assistant — An IDE extension to verify Rust programs in VS Code with Prusti. I worked on this from 2017 to 2024.
• Mendel — Another Rust verifier, specialized in verifying usages of interior mutability. I worked on this from 2022 to 2024.

Talks

• “Building User-Friendly Rust Verification Tools.” At the Rust Verification Workshop, 2024. [Slides]
• “Prusti: Deductive Verification for Rust.” At the Swiss Verification Day, 2024. [Slides] [Demo]
• “Verifying Safe Rust Clients of Internally-Unsafe Libraries.” At the Rust Verification Workshop, 2023. [Slides]
• “Leveraging Rust Types for Modular Specification and Verification.” At Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2019. [Talk]

Publications

† = All authors are listed in alphabetical order.

• Doctoral Thesis, “Enabling Rich Lightweight Verification of Rust Software.” Federico Poli. [PDF] [BIB] [DOI]
• “Reasoning about Interior Mutability in Rust using Library-Defined Capabilities.” Federico Poli, Xavier Denis, Peter Müller, Alexander J. Summers. [arXiv]
• † “The Prusti Project: Formal Verification for Rust (invited).” Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers. In NASA Formal Methods (14th International Symposium), 2022. [PDF] [BIB] [DOI]
• † “How do Programmers Use Unsafe Rust?” Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020. [PDF] [BIB] [DOI]
  • Software artifact: [DOI]
• † “Leveraging Rust Types for Modular Specification and Verification.” Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2019. [PDF] [BIB] [DOI]
  • Distinguished artifact award
  • Software artifact: [DOI]
  • Extended technical report: [PDF] [BIB] [DOI]