High consequence systems are systems where a single failure can have catastrophic consequences. Sandia National Laboratories develops high consequence systems and uses a variety of verification and validation (V&V) techniques to ensure safe, robust, and secure operation of these systems. This talk focuses on one aspect of V&V called formal methods and gives an overview of its use at Sandia. We discuss two large verification efforts at the labs: Q Framework and foundational verification in Rocq. Q Framework provides model based systems engineering verification using model checking, refinement proofs, and automated reasoning. Foundational verification includes formal proofs of C programs using the Verified Software Toolchain and CompCert. We conclude with a discussion of research projects at Sandia including automated reasoning for floating point error analysis and probabilistic programming languages for hardware fault tolerance.