Demonstrating Rigorous Digital Engineering for Nuclear Power Plant Systems 

The technology powering a nuclear power plant system’s software and hardware must be safe, correct, and secure. It would be disastrous if any adversary – whether anonymous individuals or nation-states – gained control of these systems. Galois’s first project for the Nuclear Regulatory Commission (NRC), High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS), aims to address this urgent need. 

HARDENS demonstrates Models-Based Systems Engineering (MBSE) capabilities for safety-critical nationally critical infrastructure like nuclear power plant (NPP) control and protection systems. The project uses Galois’s MBSE methodology – known as Rigorous Digital Engineering (RDE) – to create the HARDENS Reactor Trip System (RTS). The RTS is the world’s most advanced, high-assurance protection system demonstrator. The HARDENS RTS includes formally assured hardware – a three-core RISC-V System-on-Chip, automatically generated and hand-written formally verified hardware components. It also includes automatically synthesized and hand-written formally verified software.

The HARDENS demonstrator’s most informal specification starts with precise English from the NRC RFP and relevant IEEE standards. These specifications refine to formally verified properties of the hardware and software, and this refinement is completely traceable. The HARDENS RTS includes several digital twins, demonstrates co-design and co-verification using formal methods, and it uses refinement for traceability and digital threads. HARDENS’s final description and assurance case (e.g., the evidence of its correctness) is digital and physical. The entire system is exported as a single rich, hyperlinked, and auditable document.

Galois presented the final slide deck and the demonstrator to the NRC in an all-day review, incorporated their input, and delivered the final technical snapshot of all artifacts.  

You can read more details about the HARDENS project on our project page. You can also read the project documentation on Galois’s HARDENS github page.