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

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

\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. We examine reactor operators and their operating procedures, investigate the fundamental limitations of human-based operation, and review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap our work addresses.

\subsection{Current Reactor Procedures and Operation}

Nuclear plant procedures form a hierarchy: normal operating procedures govern routine operations, abnormal operating procedures handle off-normal conditions, Emergency Operating Procedures (EOPs) manage design-basis accidents, Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899
provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Their development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. This rigor, however, cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.

\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
and completeness.} Current procedure development relies on expert judgment and
simulator validation. 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. Even
computer-based procedure systems lack the formal guarantees 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
alone. Safety systems, by contrast, operate with implemented automation. Reactor
Protection Systems trip automatically on safety signals with millisecond
response times, and engineered safety features actuate automatically on accident
signals without operator action required.

The division between automated and human-controlled functions reveals hybrid control's
fundamental challenge. Highly automated systems handle reactor
protection---automatic trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
however, retain control of strategic decision-making: power level changes,
startup/shutdown sequences, mode transitions, and procedure implementation.

\subsection{Human Factors in Nuclear Accidents}

The previous subsection established that procedures lack formal verification despite rigorous development. This subsection examines the second pillar of current practice: the human operators who execute these procedures. While procedures define what to do, human operators determine when and how to apply them—an approach that introduces fundamental reliability limitations.

Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United States~\cite{operator_statistics}. These
operators divide into Reactor Operators (ROs), who manipulate reactor controls,
and Senior Reactor Operators (SROs), who direct plant operations and serve as
shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
operator requires several years of training.

Human error persistently contributes to nuclear safety incidents despite decades
of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees.
Under 10 CFR Part 55, operators hold legal authority to make critical decisions,
including departing from normal regulations during emergencies. The Three Mile
Island (TMI) accident demonstrated how personnel error, design
deficiencies, and component failures combined to cause partial meltdown. Operators
misread confusing and contradictory indications, then 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{WNA2020}. More significantly, the root cause of
all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
Fukushima Daiichi---has been identified as poor safety management and safety
culture: 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 training alone cannot overcome.} Four decades of improvements have failed to eliminate human
error. These
limitations are fundamental to human-driven control, not remediable defects.

\subsection{Formal Methods}

The previous two subsections identified the limits of current practice: procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative path: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.

\subsubsection{HARDENS}

The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
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. The NRC contracted Galois, a formal methods firm, to demonstrate that
Model-Based Systems Engineering and formal methods could design, verify, and
implement a complex protection system meeting regulatory criteria at a fraction
of typical cost. The project delivered a Reactor Trip System (RTS)
implementation with full traceability from NRC Request for Proposals and IEEE
standards through formal architecture specifications to verified software.

HARDENS employed formal methods tools and techniques across the verification
hierarchy. 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. 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 its accomplishments, HARDENS has a fundamental limitation directly
relevant to hybrid control synthesis: the project addressed only discrete
digital control logic without modeling or verifying continuous reactor dynamics.
The Reactor Trip System specification and verification covered discrete state
transitions (trip/no-trip decisions), digital sensor input processing through
discrete logic, and discrete actuation outputs (reactor trip commands). The
project did not address continuous dynamics of nuclear reactor physics. 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, not the 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 also faced deployment maturity constraints beyond the technical limitation of omitting continuous dynamics. The project produced a demonstrator system at Technology Readiness Level 2--3
(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
actual nuclear facilities, testing with real reactor systems under operational
conditions, side-by-side validation with operational analog RTS systems,
systematic failure mode testing (radiation effects, electromagnetic
interference, temperature extremes), 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, long-term reliability
under harsh environments, human-system interaction in realistic
operational contexts, and regulatory acceptance of formal methods as
primary assurance evidence.

\subsubsection{Sequent Calculus and Differential Dynamic Logic}

HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). 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
ivariant 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. 

%source: https://symbolaris.com/logic/dL.html

While dL allows for the specification of these liveness and safety properties,
actually proving them for a given hybrid system is difficult. Automated proof
assistants such as KeYmaera X exist to help develop proofs of systems using dL,
but fail for reasonably complex hybrid systems. State space explosion and
non-terminating solutions prevent creating system proofs using dL. 
%Source: that one satellite tracking paper that has the problem with the
%gyroscopes overloding and needing to dump speed all the time
Approaches have been made to alleviate
these issues for nuclear power contexts using contract and decomposition based
methods, but are far from a complete methodology to design systems with.
%source: Manyu's thesis. 
Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs. 

\textbf{LIMITATION:} \textit{Logic-based hybrid system verification has not
scaled to system design.} While dL and related approaches can verify hybrid
systems post-hoc, they require expert knowledge and have been applied only to
systems designed a priori. State space explosion prevents their use in the
design loop for complex systems like nuclear reactor startup procedures.

\subsection{Summary: The Verification Gap}

\textbf{What is the state of the art?} Current practice reveals a fundamental gap between capability and need. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and does not scale to system synthesis.

\textbf{The gap our work addresses:} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid verification—prevents autonomous nuclear control with end-to-end correctness guarantees. Closing this gap enables autonomous control that addresses the economic constraints threatening small modular reactor viability while maintaining the safety assurance the nuclear industry requires.

The next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed.