Thesis/2-state-of-the-art/state-of-art.tex

\section{State of the Art and Limits of Current Practice}

The principal aim of this research is to create autonomous reactor control
systems that are tractably safe. Understanding what is being automated requires
understanding how nuclear reactors are operated today. This section examines
reactor operating procedures, investigates limitations of human-based operation,
and reviews current formal methods approaches to reactor control systems.

\subsection{Current Reactor Procedures and Operation}

Nuclear plant operations are governed by a hierarchy of written procedures,
ranging from normal operating procedures for routine operations to Emergency
Operating Procedures (EOPs) for design-basis accidents\footnote{A
\textit{design-basis accident} is the worst-case scenario that a plant is
specifically engineered to handle safely---like a pipe break or loss of
coolant. \textit{Beyond-design-basis events} are even more extreme scenarios
that go beyond what the plant was originally designed for, like what happened
at Fukushima.} and Severe Accident Management Guidelines (SAMGs) for
beyond-design-basis events. These procedures
exist because reactor operation requires deterministic responses to a wide range
of plant conditions, from routine power changes to catastrophic failures. These
procedures must comply with 10 CFR 50.34(b)(6)(ii)\footnote{``10 CFR''
refers to Title 10 of the \textit{Code of Federal Regulations}, which governs
energy in the United States. These are the federal rules that nuclear power
plants must follow, enforced by the Nuclear Regulatory Commission (NRC).
``NUREG'' documents are technical reports published by the NRC.} and are
developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}. Procedures undergo
technical evaluation, simulator validation testing, and biennial review as part
of operator requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this
rigor, procedures fundamentally lack exhaustive verification of key safety
properties. 

\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
correctness and completeness.}  No mathematical proof exists that procedures
cover all possible plant states, that required actions can be completed within
available timeframes, or that transitions between procedure sets maintain safety
invariants. Paper-based procedures cannot ensure correct application, and even
computer-based procedure systems lack the formal guarantees that automated
reasoning could provide.

Nuclear plants operate with multiple control modes: automatic control, where
the reactor control system maintains target parameters through continuous
reactivity adjustment; manual control, where operators directly manipulate
the reactor; and various intermediate modes. In typical pressurized water
reactor operation, the reactor control system automatically maintains a
floating average temperature and compensates for power demand changes through
reactivity feedback loops\footnote{\textit{Reactivity} is a measure of how
far a reactor is from a stable chain reaction. \textit{Feedback loops}
automatically adjust the reactor's behavior---for example, as temperature
rises, the physics of the reactor naturally slow the chain reaction down.
Controllers use these feedback mechanisms to keep the reactor stable.} alone. Safety systems, by contrast, operate with
implemented automation. Reactor Protection Systems trip\footnote{A reactor \textit{trip} (also called
a \textit{SCRAM}) is an emergency shutdown---all control rods are inserted
into the reactor core within seconds to stop the chain reaction. This is the
nuclear equivalent of slamming on the brakes.} automatically on safety
signals with millisecond response times, and engineered safety features
actuate automatically on accident signals without operator action required.

This division between automated and human-controlled
functions is itself the hybrid control problem. Automated systems handle
reactor protection: trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
operators retain control of everything else: power level changes,
startup/shutdown sequences, mode transitions, and procedure
implementation.

The persistent role of human error in nuclear safety incidents---despite decades
of improvements in training and procedures---provides the most compelling
motivation for formal automated control with mathematical safety guarantees.
Operators hold legal authority under 10 CFR Part 55 to make critical
decisions~\cite{10CFR55}, including departing from normal regulations during
emergencies. This authority itself introduces risk. The Three Mile Island (TMI)
accident demonstrated how a combination of personnel error, design deficiencies,
and component failures led to partial meltdown when operators misread confusing
and contradictory readings and shut off the emergency water
system~\cite{Kemeny1979}. The President's Commission on TMI identified a
fundamental ambiguity: placing responsibility for safe power plant operations on
the licensee without formal verification that operators can fulfill this
responsibility does not guarantee safety. This tension between operational
flexibility and safety assurance remains unresolved: the person responsible for
reactor safety is often the root cause of failures.

Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus approximately
20\% to equipment failures~\cite{noauthor_human_nodate}. More significantly, the
root cause of all severe accidents at nuclear power plants---Three Mile Island,
Chernobyl, and Fukushima Daiichi---has been identified as primarily human
factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at Chinese
nuclear power plants from 2007--2020~\cite{zhang_analysis_2025} found that 53\%
of events involved active errors, while 92\% were associated with latent
errors---organizational and systemic weaknesses that create conditions for
failure.

\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
limits that cannot be overcome through training alone.} The persistent human
error contribution despite four decades of improvements demonstrates that
these limitations are fundamental rather than a remediable part of
human-driven control.

\subsection{Formal Methods}
\subsubsection{HARDENS}

The High Assurance Rigorous Digital Engineering for Nuclear Safety
(HARDENS)\footnote{HARDENS was a major U.S. government-funded project
(completed 2024) to prove that modern mathematical verification techniques
could be used for nuclear safety systems. It is the closest thing to what
Dane is proposing, but---as he explains below---it only solved half the
problem.} project represents the most advanced application of formal methods
to nuclear reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address a
fundamental dilemma: existing U.S. nuclear control rooms rely on analog
technologies from the 1950s--60s. This technology is obsolete compared to modern
control systems and incurs significant risk and cost. A U.S. Nuclear Regulatory
Commission report demonstrated that model-based systems engineering and formal
methods could design, verify, and implement a complex protection system meeting
regulatory criteria. The project delivered a Reactor Trip System (RTS)
implementation with traceability from regulatory requirements to verified
software through formal architecture specifications.

HARDENS employed formal methods tools at every level of system development, from
high-level requirements through executable models to generated code. High-level
specifications used Lando, SysMLv2, and FRET (NASA Formal Requirements
Elicitation Tool) to capture stakeholder requirements, domain engineering,
certification requirements, and safety requirements. Requirements were analyzed
for consistency, completeness, and realizability using SAT and SMT
solvers.\footnote{\textit{SAT} and \textit{SMT solvers} are computer programs
that can automatically determine whether a set of logical statements can all
be true at the same time. Think of them as extremely powerful puzzle solvers
that can check millions of combinations to find contradictions or confirm
that requirements are consistent.}
Executable formal models used Cryptol to create a behavioral model of the entire
RTS, including all subsystems, components, and limited digital twin models of
sensors, actuators, and compute infrastructure. Automatic code synthesis
generated verifiable C implementations and SystemVerilog hardware
implementations directly from Cryptol models---eliminating the traditional gap
between specification and implementation where errors commonly arise.

Despite these accomplishments, HARDENS addressed only discrete digital
control logic. The Reactor Trip System verification covered discrete state
transitions, digital sensor processing, and discrete actuation outputs. It
did not model or verify continuous reactor dynamics. Real reactor safety
depends on the interaction between continuous processes---temperature,
pressure, neutron flux---evolving in response to discrete control decisions.
HARDENS verified the discrete controller in isolation but not a
closed-loop hybrid system behavior.

\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
without continuous dynamics or hybrid system verification.} Verifying
discrete control logic alone provides no guarantee that the closed-loop
system exhibits desired continuous behavior such as stability, convergence to
setpoints, or maintained safety margins.

HARDENS produced a demonstrator system at Technology Readiness Level 2--3\footnote{\textit{Technology Readiness Levels}
(TRLs) are a 1--9 scale used by NASA and the Department of Defense to measure
how close a technology is to real-world use. TRL 1 is a basic idea on paper;
TRL 9 is a fully proven, deployed system. TRL 2--3 means ``we showed the
math works and built a basic lab prototype.'' Dane is aiming for TRL 5:
tested on real industrial hardware in realistic conditions.}
(analytical proof of concept with laboratory breadboard validation) rather than
a deployment-ready system validated through extended operational testing. The
NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
considered in development, not a finalized product, and that ``The demonstration
of its technical soundness was to be at a level consistent with satisfaction of
the current regulatory criteria, although with no explicit demonstration of how
regulatory requirements are met.'' The project did not include deployment in
%DAS 3/16/26. I double checked this quote. It's on page 4 of the HARDENS report
actual nuclear facilities, testing with real reactor systems under operational
conditions, side-by-side validation with operational analog RTS systems,
systematic failure mode testing, NRC licensing review, or human factors
validation with licensed operators in realistic control room scenarios.

\textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
validation.} While formal verification provides mathematical correctness
guarantees for the implemented discrete logic, the gap between formal
verification and actual system deployment involves myriad practical
considerations: integration with legacy systems, human-system interaction in
realistic operational contexts, and regulatory acceptance of formal methods as
primary assurance evidence remain as significant challenges.

\subsubsection{Temporal Logic and Formal Specification}

Formal verification of any system requires a precise language for stating
what the system must do. Temporal logic\footnote{\textit{Temporal logic} is a way of making precise
statements about how things change over time. Regular logic says ``the door
is open'' (true or false right now). Temporal logic can say ``the door must
\textit{always} stay open,'' ``the door will \textit{eventually} open,'' or
``the door stays open \textit{until} someone closes it.'' For reactors, this
lets us write precise rules like ``the temperature must \textit{always} stay
below 600\textdegree{}C'' or ``if pressure drops, shutdown must
\textit{eventually} happen.''}
provides this language by extending classical propositional logic with
operators that express properties over time~\cite{baier_principles_2008}. Where propositional logic can state that
a condition is true or false, temporal logic can state that a condition must
always hold, must eventually hold, or must hold until some other condition is
met. Linear temporal logic (LTL) formalizes these notions through four key
operators:
\begin{itemize}
  \item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state
  \item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states
  \item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state
  \item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes
    true
\end{itemize}
These operators allow specification of safety properties ($\mathbf{G}\neg
\textit{Unsafe}$), liveness properties ($\mathbf{F}\textit{ Target}$), and
response properties ($\mathbf{G}(\textit{Trigger} \rightarrow
\mathbf{F}\textit{ Response})$). For nuclear control, this expressiveness
captures exactly the kinds of requirements that matter: the reactor must
never enter an unsafe configuration, the system must eventually reach
operating temperature, and if coolant pressure drops, shutdown must initiate
within bounded time. These properties can be derived directly from operating
procedures and regulatory requirements, creating a formal link between
existing documentation and verifiable system behavior.

\subsubsection{Differential Dynamic Logic}

A separate line of work extends temporal logics to verify hybrid systems
directly. The result has been the field of differential dynamic
logic (dL)\footnote{\textit{Differential dynamic logic} combines temporal
logic (rules about time) with differential equations (the math that
describes continuous physical change). It is an ambitious attempt to verify
hybrid systems all at once, rather than breaking them into pieces. The
tradeoff is that it becomes very difficult to use on complex real-world
systems.}~\cite{platzer_differential_2008}. dL
introduces two additional operators into temporal logic: the box operator and
the diamond operator. The box operator \([\alpha]\phi\) states that for some
region \(\phi\), the hybrid system \(\alpha\) always remains within that
region. In this way, it is a safety invariant being
enforced for the system. The second operator, the diamond operator
\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
trajectory of \(\alpha\) that enters that region. This is a declaration of a
liveness property.


While dL allows for the specification of these liveness and safety properties,
actually proving them for a given hybrid system is quite difficult. Automated
proof assistants such as KeYmaera X~\cite{fulton_keymaera_2015} exist to help
develop proofs of systems
using dL, but so far have been insufficient for reasonably complex hybrid
systems. The main issue behind creating system proofs using dL is
non-terminating solutions. Approaches have been made to alleviate these issues
for nuclear power contexts using contract and decomposition based methods, but
do not yet constitute a complete design methodology \cite{kapuria_using_2025}.
Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs.

%Maybe a limitation here? Something about dL doesn't scale or help in design
%very much, so the limitation is that logic based hybrid system approaches
%have not been used in the DESIGN of autonomous controllers, only in the
%analysis of systems that already exist.

\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
post-hoc analysis of existing systems, not for the constructive design of
autonomous controllers.} Current dL-based approaches verify systems that
have already been designed, requiring expert knowledge to construct proofs.
They have not been applied to the synthesis of new controllers from
operational requirements.