\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. To understand what is being automated, we must
first understand how nuclear reactors are operated today. This section examines
reactor operators and the operating procedures we aim to leverage, then
investigates limitations of human-based operation, and concludes with current
formal methods approaches to reactor control 
systems.\splitnote{Good roadmap --- tells reader exactly what's 
coming.}\dasinline{Don't like ``we'' here. Sounds like
``we're going on an adventure!'' and feels jocular.
Maybe: ``To motivate this proposal, the state of
the art of nuclear reactor control, blah, and blah,
are discussed in this section.''}

\subsection{Current Reactor Procedures and Operation}

Nuclear plant procedures exist in a hierarchy: normal operating procedures for
routine operations, abnormal operating procedures for off-normal conditions,
Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
scenarios.\dasinline{This sentence is MASSIVE. Why is
there 6 lines describing different types of
procedures? WHO CARES? Need a sentence after saying
why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
development relies fundamentally on expert judgment and simulator validation
rather than formal verification. 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 formal verification of key safety 
properties.\dasinline{Does the audience know what formal
verification is at this point? Probably, but should
say differently. Maybe `exhaustive' or
`definitive'.} 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.\splitsuggest{This paragraph is doing a lot. Consider splitting: 
first paragraph on the hierarchy and compliance, second on the lack of formal 
verification. The ``No mathematical proof exists...'' sentence is powerful and 
deserves emphasis.}

\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, and even
computer-based procedure systems lack the formal guarantees that automated
reasoning could provide.\splitpolish{This repeats the ``No mathematical 
proof exists...'' sentence almost verbatim from the paragraph above. Either 
cut it from the paragraph or from the LIMITATION box.}

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.

\dasinline{After reading the next sentence, ``key safety''
can honestly just be a semicolon.}
\dasinline{Not sure what the challenge actually is
as this paragraph is written. What's the point?}
The division between automated and human-controlled functions reveals the
fundamental challenge of hybrid control. 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.\splitnote{This is the key insight — the hybrid nature is 
already there, just not formally verified.}

\subsection{Human Factors in Nuclear Accidents}

Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United 
States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
be in broader impacts about running out of ROs?
As it is here I have no idea why this is here.} 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.

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.\splitnote{Strong thesis for this subsection.}
Operators hold legal authority under 10 CFR Part 55 to make critical 
decisions,\dasinline{Cite.}
including departing from normal regulations during emergencies. 
\dasinline{Needs a connector here. Like ``But this can
in and of itself prime plants for an accident.''
Then continue.}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.\splitnote{``the person responsible for reactor safety is often the 
root cause of failures'' — devastating summary. Very effective.}

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.\splitnote{Strong empirical grounding. The Chinese plant data is a 
nice addition — shows this isn't just a Western regulatory perspective.}


\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.\splitnote{Well-stated. The ``four decades'' point drives it home.}

\subsection{Formal Methods}
\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.\dasinline{Source?}
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.\dasinline{Wordsmith this to remove the RFP and
IEEE standards language. Should just say
requirements.}

HARDENS employed formal methods tools and techniques across the verification
hierarchy.\dasinline{Zero discussion about what the
verification hierarchy is. What is a specification
or a requirement to someone who hasn't heard of
one before?} 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.\splitnote{Good technical depth on HARDENS toolchain.}

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.\dasinline{Edit these to more clearly separate
the context from the limit. The limitation should
be in the limitation.}
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 but not the closed-loop hybrid system 
behavior.\splitnote{Clear articulation of the gap your work fills.}

\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
(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.''\dasinline{Check this quote. Absolutely damning
for HARDENS if true and hilarious Galois said
this.} 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.}\dasinline{Same as before. Separate limit
from context better.} 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}
There has been additional work to do verification of hybrid systems by extending
the temporal logics 
directly.\dasinline{Need to introduce temporal logic
and FRET here first.} The result has been the field of 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.\splitfix{Typo: ``ivariant'' should be 
``invariant''} 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 quite difficult. Automated
proof assistants such as KeYmaera X 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 state space
explosion and non-terminating 
solutions.\splitsuggest{Consider adding a concrete example here — ``For 
instance, a system with N modes and M continuous state variables...'' to give 
readers a sense of the scaling problem.}
%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.\splitpolish{``but are far from a complete methodology to design systems 
with'' — awkward ending preposition. Try: ``but remain far from a complete 
design methodology'' or ``but do not yet constitute a complete design 
methodology.''}
%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. 

%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.
\splitinline{Your comment here is spot-on. You should add a LIMITATION box: 
\textit{Differential dynamic logic has been used for post-hoc analysis of 
existing systems, not for the constructive design of autonomous controllers.} 
This is exactly the gap you're filling — you're doing synthesis, not just 
verification.}