Nuclear power plants in the United States are part of what the Department of Homeland Security identifies as “nationally critical infrastructure,” a category that also includes our vast transportation network, water systems, electrical grids, and more. For decades, even as other parts of the nation’s infrastructure began using computers, American nuclear power plants avoided integrating digital systems into their control rooms, relying instead on analog systems rooted in technologies from the ‘50s and ‘60s.
“Existing nuclear power plant control systems have no computers in them,” said Galois Principal Scientist Joe Kiniry. “If you’ve watched the Simpsons and seen Homer in the control room with all the dials and stuff – that’s how they really work. The only digital components in there are PCB boards where every single piece is big enough to touch.”
The reasons for this pattern are not rooted in Luddite tendencies, but rather in a culture of rigorous safety engineering. The risks associated with shoddy nuclear engineering, as history can testify, are nothing to scoff at. The analog technology still at the heart of plant control and protection systems is well-understood and trustworthy, so why risk a change?
Yet as the years march on, the allure of “better, faster, cheaper” promised by introducing cutting-edge digital technologies has become harder to ignore. Even as demand for clean energy solutions has spurred a growing (if controversial) call to build more nuclear reactors, the cost of building has risen dramatically over time, with recent projects amassing capital costs of more than $10,000/kW. Meanwhile, the Department of Energy (DOE) estimates that “deployment at scale” of nuclear reactors (a key strategy in U.S. goals for a decarbonized grid) would require the cost of a new build to drop to around $3,600/kW. Simultaneously, the combination of technical complexity and regulatory hurdles required to build a new nuclear power plant mean that construction can drag on for decades.
Thus, the industry’s dilemma: How to reduce the cost and increase the speed of building nuclear power plants without compromising safety? One piece of that puzzle may lie in a Correct-by-Construction approach to digitizing nuclear protection and control systems.
RDE for the NRC
In 2021, the Nuclear Regulatory Commission (NRC) contacted Galois, along with several academic researchers, to explore the most secure, efficient, and practical ways to begin integrating digital technologies into plant protection and control systems. The hope was to find digital solutions that could help bring down the total cost and timeline for building nuclear power plants, but without yielding even an inch of safety or security. From those conversations emerged the High Assurance Rigorous Digital Engineering for Nuclear Safety project (known as “HARDENS” for short).
“They figured if nuclear power plants want to start using computers, we’d better figure out a way to build protection and control systems that we really believe are safe,” Kiniry explained. “They told us it’s going to be a small project, but they hoped it would help them understand what’s possible with Correct-by-Construction, model-based engineering approaches to digital instrumentation in control systems.”
On HARDENS, the NRC asked Galois to create a digital model of a fault-tolerant nuclear power plant protection system. In short: a proof of concept showing that a future-certifiable rigorous digital engineering approach could design a complex, high-assurance protection system at a fraction of the typical cost.
It was an audacious goal on its own. Yet what Galois delivered was far more.
“We built not just an RDE model, but a from scratch, soup-to-nuts, full implementation of the reactor trip system (RTS) that takes us from the government RFP, the IEEE Standards for protection systems, and a CONOPS document that describes what the system should do, all the way down to formally verified binaries and hardware,” said Kiniry.
The RTS, currently the world’s most advanced protection system demonstrator, showcases formally assured hardware, including a RISC-V System-on-Chip, and automatically generated and hand-written formally-verified hardware and software components.
What set the project apart was its commitment to traceability and rigorous assurance. The project began by taking informal specifications derived from NRC RFPs and relevant IEEE standards, and refining them into a formal architecture specification along with formally verifiable properties at the architecture and the software and hardware source level. This refinement process ensures that every aspect of the hardware and software is traceable, creating a digital thread that integrates every stage of development, and allowing for easy auditing of the final description and assurance case.
This result was far more than the NRC had asked for or expected, built entirely on open-source tools, and delivered in a mere nine months at a tiny fraction of the cost of a typical control and protection system.
“Ultimately, the NRC wants to be in a place where they can wisely use digital technology for control that’s secure from adversaries, that saves them time and money, and that makes certification easier,” Kiniry said. “They want to move from control rooms costing $500M to build and certify, to costing a tenth of that, and taking a tenth of the time. And they want all this because many of them truly believe that the future of humanity depends on nuclear power working safely.”
With the HARDENS project, Galois showed that such a dream is imminently possible.
Looking Ahead
Since the bulk of the work finished in June 2022, HARDENS’ success has slowly gained momentum and attention internationally. In 2023, the Institute for Energy Technology (IFE)’s Halden Workshops, a bi-annual year-long symposium for nuclear industry professionals, used HARDENS as a case study to explore the potential of using correct-by-construction and formal methods-based techniques to eliminate heterogeneous redundancy—a method where multiple providers build the same subsystem to ensure reliability. Kiniry, representing Galois, spoke at nearly every symposium meeting.
While the project has received a spectrum of reactions, from conservative skepticism to enthusiastic support, it is undeniably paving the way for future advancements. Galois Principal Researcher Danielle Stewart is currently working with the NRC on a new project called Safety Engineering Framework for Model-based Evaluation (SAFEFRAME). This project will extend the HARDENS case study with safety-specific requirements and analysis, illustrating a Correct-by-Construction approach to designing nuclear systems. A key aspect of the project is to aid the NRC in developing an understanding of how a Correct-by-Construction approach could be analyzed during the review and certification processes.
“We have shown that we can use formal methods and RDE to build formally-assured subsystems,” said Stewart. “Now we want to show how these formally-assured systems can be reviewed by relevant authorities and be certified for use in the nuclear energy field.”
It is clear that the nuclear power industry’s evolution will take time—with significant changes likely requiring a decade or more to solidify—but projects like HARDENS are a small push in the right direction, and a hopeful glimpse into a future where alternative energy solutions are safer, cheaper, and faster to build.