VeriFast is a research prototype tool for modular formal verification of correctness properties of single-threaded and multithreaded C, Java, and Rust programs. It uses separation logic to specify and verify properties such as memory safety, functional correctness, termination, deadlock freedom, and security properties. The tool provides frontends for multiple languages, an SMT-based verifier (primarily Z3), and an IDE. It has been applied to real-world code including Java Card applets, Linux kernel drivers, cryptographic protocols, and concurrent data structures. The codebase is well-structured with a core OCaml verifier, language-specific frontends (C/C++ via Clang, Rust via MIR, Java via bytecode), and a rich set of examples and test suites.