Verifying Rust code with Verus

Hance, Travis

doi:10.34727/2026/isbn.978-3-85448-093-8_1

Record link:

http://hdl.handle.net/20.500.12708/230444
https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_1

Title:

Citation:

Hance, T. (2026). Verifying Rust code with Verus. In B. Dutertre & B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_1

reposiTUm DOI:

10.34727/2026/isbn.978-3-85448-093-8_1

CatalogPlus:

AC17999067

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Hance, Travis

Editors:

Dutertre, Bruno
Könighofer, Bettina

Organisational Unit:

E000 - Technische Universität Wien

Series:

Conference Series: Formal Methods in Computer-Aided Design

Published in:

Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026

Date (published):

Sep-2026

Number of Pages:

Publisher:

TU Wien Academic Press

Peer reviewed:

Yes

Keywords:

formal methods; computer-aided system design; hardware and system verification

Abstract:

I will introduce Verus, an open-source, Rust-based verification tool aimed at concurrent software and systems software, which I develop together with a number of collaborators in academia and industry. Verus has spawned a number of publications on a range of verified systems, is already seeing industrial use at Microsoft and Amazon, and has been the subject of a number of experiments on generating proofs with AI. In this tutorial, I will give an overview of Verus and what it can do, and why we invented it compared to the previous state-of-the-art approaches to program verification. I will give a tutorial on how to get started with Verus, and I will illustrate how we approach the various challenges of verification through a number of examples.

Is part of:

10.34727/2026/isbn.978-3-85448-093-8

Research Areas:

Logic and Computation: 40%
Computer Engineering and Software-Intensive Systems: 40%
Computer Science Foundations: 20%

Science Branch:

1020 - Informatik: 100%

License:

CC BY 4.0