The Prusti Project: Formal Verification for Rust

Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

12 Downloads (Pure)


Rust is a modern systems programming language designed to offer both performance and static safety. A key distinguishing feature is a strong type system, which enforces by default that memory is either shared or mutable, but never both. This guarantee is used to prevent common pitfalls such as memory errors and data races. It can also be used to greatly simplify formal verification, as we demonstrated by developing the Prusti verifier, which can verify rich correctness properties of Rust programs with a very modest annotation overhead. In this paper, we provide an overview of the Prusti project. We outline its main design goals, illustrate examples of its use, and discuss important outcomes from the perspectives of a user, a verification expert, and a tool developer.

Original languageEnglish
Title of host publicationNASA Formal Methods
EditorsJyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
Publication date2022
ISBN (Print)9783031067723
Publication statusPublished - 2022
Event14th International Symposium on NASA Formal Methods - Hameetman Center - Caltech Campus, Pasadena, United States
Duration: 24 May 202227 May 2022


Conference14th International Symposium on NASA Formal Methods
LocationHameetman Center - Caltech Campus
Country/TerritoryUnited States
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13260 LNCS


  • Deductive verification
  • Rust
  • Separation logic


Dive into the research topics of 'The Prusti Project: Formal Verification for Rust'. Together they form a unique fingerprint.

Cite this