Abstract: Formal methods tools that provide mathematical proof of system properties have improved dramatically in their power and capabilities. As part of DARPA's Cyber Assured Systems Engineering (CASE) program, our team has developed a model-based systems engineering environment called BriefCASE that integrates formal methods at all levels of system design. Our methodology and tools enable systems engineers to address cybersecurity concerns early in the development of complex high-assurance systems.

Abstract: In the **High Assurance Rigorous Digital Engineering for Nuclear Safety** (HARDENS) project, Galois has developed a high-assurance, safety-critical demonstration system for the Nuclear Regulatory Commission using Rigorous Digital Engineering (RDE).  The system in question is a Digital Instrumentation and Control (DI&C) system for Nuclear Power Plants (NPPs), and is called the Reactor Trip System (RTS).