\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. But, to understand what exactly is being automated, it is important to understand how nuclear reactors are operated today. First, the reactor operator themselves is discussed. Then, operating procedures that we aim to leverage later are examined. Next, limitations of human-based operation are investigated, while finally we discuss current formal methods based approaches to building reactor control systems. \subsection{Current Reactor Procedures and Operation} Current generation nuclear power plants employ 3,600+ active NRC-licensed reactor operators in the United States. These operators are divided 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 2+ ROs with at least one SRO for current generation units. To become a reactor operator, an individual might spend up to six years to pass required training~\cite{princeton}. The role of human operators is paradoxically both critical and problematic. Operators hold legal authority under 10 CFR Part 55 to make critical decisions including departing from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how ``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 and accountability for safe power plant operations...on the licensee in all circumstances'' without formal verification that operators can fulfill this responsibility under all conditions~\cite{Kemeny1979}. This tension between operational flexibility and safety assurance remains unresolved in current practice. 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. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using guidance from NUREG-0899~\cite{NUREG-0899}, but their development process 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}. Despite these rigorous development processes, procedures fundamentally lack formal verification of key safety properties. There is no mathematical proof that procedures cover all possible plant states, that required actions can be completed within available timeframes under all scenarios, 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, 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 rod adjustment, manual control where operators directly manipulate control rods, and various intermediate modes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for changes in power demand with reactivity feedback loops alone. Safety systems instead 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 current division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems handle reactor protection like automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control. Human operators, however, retain control of strategic decision-making such as power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. %%%NEED MORE \textbf{LIMITATION:} \textit{Current practice treats continuous plant dynamics and discrete control logic separately.} No application of hybrid control theory exists that could provide mathematical guarantees across mode transitions, verify timing properties formally, or optimize the automation-human interaction trade-off with provable safety bounds. \subsection{Human Factors in Nuclear Accidents} The persistent role of human error in nuclear safety incidents, despite decades of improvements in training and procedures, provides perhaps the most compelling motivation for formal automated control with mathematical safety guarantees. Multiple independent analyses converge on a striking statistic: \textbf{70--80\% of all nuclear power plant events are attributed to human error} versus approximately 20\% to equipment failures~\cite{DOE-HDBK-1028-2009,WNA2020}. More significantly, the International Atomic Energy Agency concluded that ``human error was the root cause of all severe accidents at nuclear power plants''---a categorical statement spanning Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{IAEA-severe-accidents}. A detailed analysis of 190 events at Chinese nuclear power plants from 2007--2020~\cite{Wang2025} found that 53\% of events involved active errors while 92\% were associated with latent errors (organizational and systemic weaknesses that create conditions for failure). The persistence of this 70--80\% human error contribution despite four decades of continuous improvements in operator training, control room design, procedures, and human factors engineering. This suggests fundamental cognitive limitations rather than remediable deficiencies. The Three Mile Island Unit 2 accident on March 28, 1979 remains the definitive case study in human factors failures in nuclear operations. The accident began at 4:00 AM with a routine feedwater pump trip, escalating when a pressure-operated relief valve (PORV) stuck open---draining reactor coolant---but control room instrumentation showed only whether the valve had been commanded to close, not whether it actually closed. When Emergency Core Cooling System pumps automatically activated as designed, operators made the fateful decision to shut them down based on their incorrect assessment of plant conditions. The result was a massive loss of coolant accident and the core quickly began to overheat. During the emergency, operators faced more than 100 simultaneous alarms, overwhelming their cognitive capacity~\cite{Kemeny1979}. The core suffered partial meltdown with \textbf{44\% of the fuel melting} before the situation was stabilized. Quantitative risk analysis revealed the magnitude of failure in existing safety assessment methods: the actual core damage probability was approximately 5\% per year while Probabilistic Risk Assessment had predicted 0.01\% per year---a \textbf{500-fold underestimation}. This dramatic failure demonstrated that human reliability could not be adequately assessed through expert judgment and historical data alone. %%%SOURCE??? Human Reliability Analysis (HRA) methods developed over four decades quantify human error probabilities and performance shaping factors. The SPAR-H method represents current best practice, providing nominal Human Error Probabilities (HEPs) of \textbf{0.01 (1\%) for diagnosis tasks} and \textbf{0.001 (0.1\%) for action tasks} under optimal conditions~\cite{NUREG-CR-6883}. However, these nominal error rates degrade dramatically under realistic accident conditions: inadequate available time increases HEP by \textbf{10-fold}, extreme stress by \textbf{5-fold}, high complexity by \textbf{5-fold}, missing procedures by \textbf{50-fold}, and poor ergonomics by \textbf{50-fold}. Under combined adverse conditions typical of severe accidents, human error probabilities can approach \textbf{0.1 to 1.0 (10\% to 100\%)}---essentially guaranteed failure for complex diagnosis tasks~\cite{NUREG-2114}. Rasmussen's influential 1983 taxonomy~\cite{Rasmussen1983} divides human errors into skill-based (highly practiced responses, HEP $10^{-3}$ to $10^{-4}$), rule-based (following procedures, HEP $10^{-2}$ to $10^{-1}$), and knowledge-based (novel problem solving, HEP $10^{-1}$ to 1). Severe accidents inherently require knowledge-based responses where human reliability is lowest. Miller's classic 1956 finding~\cite{Miller1956} that working memory capacity is limited to 7$\pm$2 chunks explains why Three Mile Island's 100+ %WHAT IS A CHUNK? simultaneous alarms exceeded operators' processing capacity. \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits that cannot be overcome through training alone.} Response time limitations constrain human effectiveness---reactor protection systems must respond in milliseconds, 100--1000 times faster than human operators. Cognitive biases systematically distort judgment: confirmation bias, overconfidence, and anchoring bias are inherent features of human cognition, not individual failings~\cite{Reason1990}. The persistent 70--80\% human error contribution despite four decades of improvements demonstrates that these limitations are fundamental rather than remediable. \subsection{HARDENS and Formal Methods} The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project, completed by Galois, Inc. for the U.S. Nuclear Regulatory Commission in 2022, represents the most advanced application of formal methods to nuclear reactor control systems to date---and simultaneously reveals the critical gaps that remain. \subsubsection{Rigorous Digital Engineering Demonstrated Feasibility} HARDENS aimed to address the nuclear industry's fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s, making construction costs exceed \$500 million and timelines stretch to decades. The NRC contracted Galois 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 far beyond its scope, creating what Galois describes as ``the world's most advanced, high-assurance protection system demonstrator.'' Completed in \textbf{nine months at a tiny fraction of typical control system costs}~\cite{Kiniry2022}, the project produced a complete Reactor Trip System (RTS) implementation with full traceability from NRC Request for Proposals and IEEE standards through formal architecture specifications to formally verified binaries and hardware running on FPGA demonstrator boards. Principal Investigator Joseph Kiniry led the team in applying Galois's Rigorous Digital Engineering methodology combining model-based engineering, digital twins with measurable fidelity, and applied formal methods. The approach integrates multiple abstraction levels---from semi-formal natural language requirements through formal specifications to verified implementations---all maintained as integrated artifacts rather than separate documentation prone to divergence. \subsubsection{Comprehensive Formal Methods Toolkit Provided Verification} HARDENS employed an impressive array of formal methods tools and techniques across the verification hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA JPL's Formal Requirements Elicitation Tool) to capture stakeholder requirements, domain engineering, certification requirements, and safety requirements. Requirements were formally analyzed for \textbf{consistency, completeness, and realizability} using SAT and SMT solvers---verification that current procedure development methods lack. Executable formal models employed Cryptol to create an executable behavioral model of the entire RTS including all subsystems, components, and formal digital twin models of sensors, actuators, and compute infrastructure. Automatic code synthesis generated formally verifiable C implementations and System Verilog hardware implementations directly from Cryptol models---eliminating the traditional gap between specification and implementation where errors commonly arise. Formal verification tools included SAW (Software Analysis Workbench) for proving equivalence between models and implementations, Frama-C for C code verification, and Yosys for hardware verification. HARDENS verified both automatically synthesized and hand-written implementations against their models and against each other, providing redundant assurance paths. This multi-layered verification approach represents a quantum leap beyond current nuclear I\&C verification practices, which rely primarily on testing and simulation. HARDENS demonstrated that \textbf{complete formal verification from requirements to implementation is technically feasible} for safety-critical nuclear control systems. \subsubsection{Critical Limitation: Discrete Control Logic Only} Despite its impressive accomplishments, HARDENS has a fundamental limitation directly relevant to hybrid control synthesis: \textbf{the project addressed only discrete digital control logic without modeling or verifying continuous reactor dynamics}. The Reactor Trip System specification and formal verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). The system correctly implements the digital control logic for reactor protection with mathematical guarantees. However, the project did not address continuous dynamics of nuclear reactor physics including neutron kinetics, thermal-hydraulics, xenon oscillations, fuel temperature feedback, coolant flow dynamics, and heat transfer---all governed by continuous differential equations. Real reactor safety depends on the interaction between continuous processes (temperature, pressure, neutron flux evolving according to differential equations) and discrete control decisions (trip/no-trip, valve open/close, pump on/off). HARDENS verified the discrete controller in isolation but not the closed-loop hybrid system behavior. \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without continuous dynamics or hybrid system verification.} Hybrid automata, differential dynamic logic, or similar hybrid systems formalisms would be required to specify and verify properties like ``the controller maintains core temperature below safety limits under all possible disturbances''---a property that inherently spans continuous and discrete dynamics. 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. \subsubsection{Experimental Validation Gap Limits Technology Readiness} The second critical limitation is \textbf{absence of experimental validation} in actual nuclear facilities or realistic operational environments. HARDENS produced a demonstrator system at Technology Readiness Level 3--4 (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{Kiniry2022}: ``All material is considered in development and not a finalized product'' and ``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), actual NRC licensing review, or human factors validation with licensed nuclear operators in realistic control room scenarios. \textbf{LIMITATION:} \textit{HARDENS achieved TRL 3--4 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. \subsection{Research Imperative: Formal Hybrid Control Synthesis} Three converging lines of evidence establish an urgent research imperative for formal hybrid control synthesis applied to nuclear reactor systems. \textbf{Current reactor control practices} reveal fundamental gaps in verification. Procedures lack mathematical proofs of completeness or timing adequacy. Mode transitions preserve safety properties only informally. Operator decision-making relies on training rather than verified algorithms. The divide between continuous plant dynamics and discrete control logic has never been bridged with formal methods. Despite extensive regulatory frameworks developed over six decades, \textbf{no mathematical guarantees exist} that current control approaches maintain safety under all possible scenarios. \textbf{Human factors in nuclear accidents} demonstrate that human error contributes to 70--80\% of nuclear incidents despite four decades of systematic improvements. The IAEA's categorical statement that ``human error was the root cause of all severe accidents'' reveals fundamental cognitive limitations: working memory capacity of 7$\pm$2 chunks, response times of seconds to minutes versus milliseconds required, cognitive biases immune to training, stress-induced performance degradation. Human Reliability Analysis methods document error probabilities of 0.001--0.01 under optimal conditions degrading to 0.1--1.0 under realistic accident conditions. These limitations \textbf{cannot be overcome through human factors improvements alone}. \textbf{The HARDENS project} proved that formal verification is technically feasible and economically viable for nuclear control systems, achieving complete verification from requirements to implementation in nine months at a fraction of typical costs. However, HARDENS addressed only discrete control logic without considering continuous reactor dynamics or hybrid system verification, and the demonstrator achieved only TRL 3--4 without experimental validation in realistic nuclear environments. These limitations directly define the research frontier: \textbf{formal synthesis of hybrid controllers that provide mathematical safety guarantees across both continuous plant dynamics and discrete control logic}. The research opportunity is clear. Nuclear reactors are quintessential hybrid cyber-physical systems where continuous neutron kinetics, thermal-hydraulics, and heat transfer interact with discrete control mode decisions, trip logic, and valve states. Current practice treats these domains separately---reactor physics analyzed with simulation, control logic verified through testing, human operators expected to integrate everything through procedures. \textbf{Hybrid control synthesis offers the possibility of unified formal treatment} where controllers are automatically generated from high-level safety specifications with mathematical proofs that guarantee safe operation across all modes, all plant states, and all credible disturbances. Recent advances in hybrid systems theory---including reachability analysis, barrier certificates, counterexample-guided inductive synthesis, and satisfiability modulo theories for hybrid systems---provide the theoretical foundation. Computational advances enable verification of systems with continuous state spaces that were intractable a decade ago. The confluence of mature formal methods, powerful verification tools demonstrated by HARDENS, urgent safety imperatives documented by persistent human error statistics, and fundamental gaps in current hybrid dynamics treatment creates a compelling and timely research opportunity.