This document describes the use of the RISC ProofNavigator, an interactive proving assistant for program and system reasoning developed at the Research Institute for Symbolic Computation (RISC).
