proof assistant and HOL (proof assistant). In comparison to the program analysis work, these tools require more in the way of human effort but prove deeper properties, up to functional correctness. A proof of the FSCQ file system where the specification includes behaviour under crashes as well as normal operation. This work won the best paper award at the 2015 Symposium on Operating System Principles. Verification of a large fragment of the Rust type system and some of its standard libraries in the RustBelt project using the Iris framework for separation logic in The Coq proof assistant. Verification of an OpenSSL implementation of a cryptographic authentication algorithm, utilizing verifiable C Verification of key modules of a commercial OS kernel, the μC/OS-II kernel, the first commercial pre-emptive kernel to have been verified. Other examples include the Ynot library for the Coq proof assistant; the Holfoot embedding of Smallfoot in HOL; Fine-grained Concurrent Separation Logic, and Bedrock (a Coq library for low-level programming). In Between. Many tools require more user intervention than program analyses, in that they expect the user to input assertions such as pre/post specs for functions or loop invariants, but after this input is given they attempt to be fully or almost fully automatic; this mode of verification goes back to classic works in the 1970s such as J King's verifier, and the Stanford Pascal Verifier. This style of verifier has recently been called auto active verification, a term which intends to evoke the way of interacting with a verifier via an assert-check loop, analogous to the interaction between a programmer and a type-checker. The very first Separation Logic verifier, Smallfoot, was in this in-between category. It required the user to input pre/post specs, loop invariants, and resource invariants for locks. It introduced a method of symbolic execution, as well as an automatic way to infer frame axioms. Smallfoot included Concurrent Separation Logic. SmallfootRG is a verifier for a marriage of separation logic and the classic rely/guarantee method for concurrent programs. Heap Hop implements a separation logic for message passing, following the ideas in Singularity (operating system). VeriFast is an advanced current tool in the in-between category. It has demonstrated proofs ranging from object-oriented patterns to highly concurrent algorithms and to systems programs. Viper is a state-of-the-art automated verification infrastructure for permission-based reasoning. It mainly consists of a programming language and two verification backends, one based on symbolic execution