[Quick intros] [Proofs done] [Binaries] [User interfaces] [Compiling] [Documentation] [Getting help] [Acknowledgements] [Mailing lists] [Third-party resources]

VeriFast

By Bart Jacobs*, Jan Smans*, and Frank Piessens*, with contributions by Pieter Agten*, Cedric Cuypers*, Lieven Desmet*, Niels Mommen*, Jan Tobias Muehlberg*, Willem Penninckx*, Pieter Philippaerts*, Nima Rahimi Foroushaani*, Amin Timany*, Thomas Van Eyck*, Gijs Vanspauwen*, Frédéric Vogels*, and external contributors

* imec-DistriNet research group, Department of Computer Science, KU Leuven - University of Leuven, Belgium

VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C, Rust and Java programs annotated with preconditions and postconditions written in separation logic. To express rich specifications, the programmer can define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To verify these rich specifications, the programmer can write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low.

The VeriFast source code and binaries are released under the MIT license.

Quick intros

• A quick introduction to VeriFast for C
• A quick introduction to VeriFast for Rust

Proofs done

Some of the more notable proofs done with VeriFast (with caveats) include:

• A proof of memory safety and thread safety of the Linux boot protocol keyboard driver
• A proof of absence of array index out of bounds exceptions, null pointer exceptions, and invalid API calls in (a mock-up of) the Java Card code running on the Belgian electronic identity card
• A modular proof of memory safety, thread safety, and termination of a cohort lock implemented on top of ticketlocks, themselves implemented using busy waiting, and using lock handoff
• Proofs of integrity and confidentiality of a number of simple cryptographic protocols implemented in C using the byte buffer-based APIs of mbed TLS (as opposed to a high-level "symbolic" API).
• A proof of a floating-point algorithm for computing the square root, taking into account rounding (but not overflow or underflow).
• Termination of some small Java programs involving dynamic binding (a.k.a. virtual method calls) and/or concurrency.
• Jayanti's optimal snapshot algorithm, using prophecies
• A concurrent set implemented using lock coupling (a.k.a. hand-over-hand locking).
• A modular proof of a fine-grained concurrent Multiple Compare And Swap (MCAS) algorithm built on top of a Restricted Double Compare Single Swap algorithm, using helping.
• Termination of various concurrent programs using monitors and condition variables
• Some small purely unsafe (i.e. C-style) Rust programs, including a constant-space tree marking algorithm
• A partial proof of the Rust standard library's LinkedList and RawVec abstractions
• Proofs of simplified versions of Rust's Cell, Mutex, Rc, Arc, and RefCell abstractions

Binaries

Within an hour after each push to the master branch, binary packages become available here.

These "nightly" builds are very stable and are recommended. Still, named releases are available here. (An archive of older named releases is here.)

Simply extract the files from the archive to any location in your filesystem. All files in the archive are in a directory named verifast-COMMIT where COMMIT describes the Git commit. For example, on Linux:

tar xzf ~/Downloads/verifast-nightly.tar.gz
cd verifast-<TAB>  # Press Tab to autocomplete
bin/vfide examples/java/termination/Stack.jarsrc  # Launch the VeriFast IDE with the specified example
./test.sh  # Run the test suite (verifies all examples)

Note (macOS): To avoid GateKeeper issues, before opening the downloaded archive, remove the com.apple.quarantine attribute by running

sudo xattr -d com.apple.quarantine ~/Downloads/verifast-nightly-osx.tar.gz

Supply chain security: The CI workflow creates GitHub Artifact Attestations for these binaries, so that you can verify that they were generated by a GitHub Actions workflow triggered by a push to this repository. To do so, install the GitHub CLI and run

gh attestation verify verifast-21.04-352-gbeb57a82-macos.tar.gz --repo verifast/verifast

To check for a particular commit SHA, run

[ "$(gh attestation verify verifast-21.04-352-gbeb57a82-macos.tar.gz --repo verifast/verifast --format json --jq '.[0].verificationResult.signature.certificate.sourceRepositoryDigest')" = "beb57a820915409f71dbc2a802985e291e60e12d" ]

User interfaces

We offer the following user interfaces:

• The VeriFast IDE (at bin/vfide in the distribution)
• The VeriFast VS Code Extension
• The VeriFast command-line tool (at bin/verifast in the distribution)

Compiling

• Windows
• Linux
• macOS

Documentation

• The VeriFast Tutorial (for C)
• Verifying purely unsafe Rust programs with VeriFast: a tutorial
• A tour of the RawVec proof (Rust)
• A tour of the LinkedList proof (Rust)
• Featherweight VeriFast (Slides, handouts, Coq proof)
• Scientific papers on the various underlying ideas
• VeriFast Docs (under construction) with a nascent FAQ and a grammar for annotated C/Java source files
• The VeriFast for Rust Reference (under construction)

Getting help

The maintainer (and, perhaps, other VeriFast users and enthusiasts as well) can be reached for informal chat in the VeriFast Zulip chatroom.

Acknowledgements

Dependencies

We gratefully acknowledge the authors and contributors of the following software packages.

Bits that we ship in our binary packages

• OCaml
• OCaml-Num
• Lablgtk
• GTK+ and its dependencies (including GLib, Cairo, Pango, ATK, gdk-pixbuf, gettext, fontconfig, freetype, expat, libpng, zlib, Harfbuzz, and Graphite)
• GtkSourceView
• The excellent Z3 theorem prover by Leonardo de Moura and Nikolaj Bjorner at Microsoft Research, and co-authors

Software used at build time

• findlib, ocamlbuild, camlp4, valac
• Cygwin, Homebrew, Debian, Ubuntu
• The usual infrastructure: GNU/Linux, GNU make, gcc, etc.

Infrastructure

We gratefully acknowledge the following infrastructure providers.

• GitHub
• The Zulip team chat app

Funding

This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen), by the EU FP7 projects SecureChange, STANCE, ADVENT, and VESSEDIA, by Microsoft Research Cambridge as part of the Verified Software Initiative