VeriFast checks C, Rust and Java against separation logic annotations

What the verifier actually checks

VeriFast is described as 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. The properties in question are the ones a separation logic encodes naturally, namely who owns which memory and what has to hold for an operation to be safe. Richer specifications are possible. The programmer can define inductive datatypes, primitive recursive pure functions over those datatypes, and abstract separation logic predicates, and to verify such a specification the programmer writes lemma functions, which are functions that exist only as proofs that their precondition implies their postcondition. The verifier checks that those lemma functions terminate and have no side effects. The authors are Bart Jacobs, Jan Smans and Frank Piessens, with contributions from a long list of colleagues and external contributors, all at the imec-DistriNet research group in the Department of Computer Science at KU Leuven.

Why the absence of search is the interesting part

The README makes one claim about performance that is worth isolating, because it is unusual in this field: since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low. That is a design constraint rather than a benchmark result, and it changes what the tool can be used for. A verifier that searches can find bugs you did not write a specification for, and it can also take an unbounded amount of time on a hard obligation. A verifier that does not search is fast, but it can only discharge the obligations you actually wrote, and the moment you write a specification the tool cannot check in the given manner, you get an error rather than a slow answer. For a modular style of work, where each function carries its own contract and the contracts are checked independently, that trade is usually the right one.

The proofs that have been done, and what they show

The README lists notable proofs, with the caveat attached. There is a proof of memory safety and thread safety of the Linux boot protocol keyboard driver, and proofs 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. On concurrency there is a modular proof of memory safety, thread safety and termination of a cohort lock built on ticket locks that themselves use busy waiting and lock handoff, a proof of a concurrent set implemented using lock coupling, and a modular proof of a fine-grained concurrent Multiple Compare And Swap algorithm built on a Restricted Double Compare Single Swap algorithm using helping. Jayanti's optimal snapshot algorithm is proved using prophecies, and there are termination proofs for various concurrent programs using monitors and condition variables. On the cryptographic side there are proofs of integrity and confidentiality for a number of simple protocols implemented in C on the byte buffer-based APIs of mbed TLS rather than a symbolic API, and a floating-point proof of a square root algorithm that takes rounding into account but not overflow or underflow. The Rust side is partial: a partial proof of the standard library's LinkedList and RawVec, proofs of simplified versions of Cell, Mutex, Rc, Arc and RefCell, and some small purely unsafe Rust programs.

Downloading a nightly build and running the examples

Within an hour after each push to the master branch, binary packages are published under the nightly release tag, and the README says those builds are very stable and are the ones recommended, with named releases also available and an archive of older named releases kept separately. The archives are self-contained: all files sit in a directory named verifast-COMMIT, and on Linux the sequence is:

    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)

The test script is the interesting part of that list, because it verifies every example in the tree, which is a quick way to confirm that a build works before you trust it on your own code. On macOS there is one extra step, removing the quarantine attribute from the downloaded archive with sudo xattr -d com.apple.quarantine on the tarball, to avoid GateKeeper issues.

Verifying the binaries themselves

The supply chain section is short and specific. The CI workflow creates GitHub Artifact Attestations for the binaries, so that you can verify they were generated by a GitHub Actions workflow triggered by a push to the repository. To do that you install the GitHub CLI and run:

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

For a tool whose whole purpose is to convince you that a program is correct, being able to check where the binary came from is a reasonable thing to want, and the fact that the project provides the mechanism rather than asking you to trust the download page is a good sign. The named release in that example, 21.04-352, also shows the versioning scheme, which encodes a year and month plus a commit count.

What is in the tree, and what it takes to build

The repository is a large research codebase and the layout tells you what building it involves. There are separate build systems rather than one: build.ml and build-helper.ml drive an OCaml build, build.sh and configure are shell entry points, config.sh and setenv.sh set the environment, and setup-build.sh and setup-devcontainer.sh prepare a working tree. The dependencies are handled by a make_vfdeps directory with a matching install-vfdeps.sh and a win32 variant, so the SMT solver and the other external pieces are fetched rather than assumed. There is a nix/ directory with flake.nix and flake.lock, a .devcontainer/ directory, and a rust-toolchain.toml for the Rust side. Platform-specific readme files exist for Linux, macOS and Windows, with README.Z3v4.5.md documenting the Z3 version, plus separate setup scripts for Windows and a GNUmakefile.settings.example. The examples/ tree is where the real content is, with hundreds of C files covering the language features, and there are Rust tutorials, a javacard_tutorial directory, docs/, help/, tests/ and a tutorial_solutions/ directory. The source and binaries are released under the MIT licence.

Where VeriFast is the wrong tool

Three cases. The first is a codebase nobody will annotate, because the value of the tool is in the specifications you write, and if the annotations are not going to be written the tool has nothing to check. The second is a project that wants whole-program verification of a large system, since VeriFast's design is modular and its strength is discharging local obligations, and the README's own list of what has been proved is a list of components and algorithms rather than of complete systems. The third is a team that needs a supported release with a changelog and a compatibility promise, since the recommended artifact is a nightly build produced within the hour of each push. Against a general-purpose SMT-based verifier such as an SMT-based reachability tool, the difference in approach is that VeriFast uses a separation logic that understands ownership, so the obligations it produces are about memory rather than about paths through the program, and the price is that you must express your specification in that logic rather than in a first-order encoding.

Editorial conclusion

VeriFast is a good fit for a research group or a systems team willing to annotate code by hand, because the absence of search is what makes it practical on a real program rather than a toy, and the proof obligations it produces are local enough to discharge one function at a time. It is a poor fit for a codebase nobody will annotate, since the work is in the annotations rather than in the tool, and it is a poor fit for a team that needs a versioned, supported release, because the recommended artifact is a nightly build. Check three things before you start: that you can accept a research prototype as your verifier, which is how the project describes itself, that you have the dependencies for the language you want to check, since the tree carries separate install scripts for the vfdeps, and that you read the soundness document, because the project's own claim about what it proves is bounded by that file rather than by the feature list.

Frequently asked questions

Official sources

1. Issues
2. README
3. Releases
4. verifast/verifast on GitHub