Multi-level editorial pass: tactical, operational, strategic improvements

Tactical (sentence-level):
- Applied Gopen's Sense of Structure principles
- Improved topic-stress positioning
- Strengthened verb choice, clarified active/passive voice usage
- Broke up overly long sentences for readability
- Enhanced topic strings between sentences

Operational (paragraph/section-level):
- Improved flow and transitions between paragraphs
- Enhanced coherence within sections
- Clarified connections between subsections
- Split complex sentences for better readability

Strategic (document-level):
- Strengthened Heilmeier catechism alignment
- Made 'What is new?' and 'Why will it succeed?' answers more explicit
- Added enumerated lists for key innovations
- Improved section-to-section transitions
- Ensured each section explicitly answers its assigned Heilmeier questions

1-goals-and-outcomes/v1.tex

@@ -1,34 +1,21 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control
+This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
-systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability.
 Control system failures risk economic losses, service interruptions,
 or radiological release.
 % Known information
-Nuclear plant operations rely on extensively trained human operators
+Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control. When operators switch between different control modes, plant conditions and procedural guidance inform their decisions.
-who follow detailed written procedures and strict regulatory requirements to
-manage reactor control. Plant conditions and procedural guidance inform their decisions when they switch between different control modes.
 % Gap
-This reliance on human operators prevents autonomous control and
+This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs that far exceed those of conventional plants, threatening economic viability. The nuclear industry needs autonomous control systems that manage complex operational sequences safely without constant human supervision while providing assurance equal to or exceeding that of human-operated systems.
-creates a fundamental economic challenge for next-generation reactor designs.
-Small modular reactors face per-megawatt staffing costs that far
-exceed those of conventional plants, threatening economic viability.
-The nuclear industry needs autonomous control systems that can manage complex
-operational sequences safely without constant human supervision while providing
-assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-We combine formal methods with control theory to build hybrid control
+We combine formal methods with control theory to build hybrid control systems that are correct by construction.
-systems that are correct by construction.
 % Rationale
-Hybrid systems mirror how operators work: discrete
+Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions. Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. No existing approach provides end-to-end correctness guarantees.
-logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions.
-Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. This gap prevents end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
 from written operating procedures and verifying continuous behavior between

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

@@ -4,8 +4,7 @@
 
 \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
+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. 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}. However, 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. Yet this rigor 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.
-provides development guidance~\cite{NUREG-0899, 10CFR50.34}. However, 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, but this rigor 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
@@ -37,7 +36,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
+Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -47,10 +46,7 @@ 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
+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 authority to depart from normal regulations during emergencies. The Three Mile
-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 combine to cause disaster. Operators
 misread confusing and contradictory indications, then shut off the emergency water
@@ -61,12 +57,7 @@ responsibility does not guarantee safety. This tension between operational
 flexibility and safety assurance remains unresolved—the person responsible for
 reactor safety often becomes the root cause of failures.
 
-Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of
+Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, compared to approximately 20\% for equipment failures~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
-nuclear power plant events, compared to approximately
-20\% for equipment failures~\cite{WNA2020}. More significantly, poor safety management and safety
-culture—primarily human factors—caused
-all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and
-Fukushima Daiichi~\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
@@ -80,7 +71,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The limitations are now clear: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach: 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.
+Two limitations are now clear: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach. They provide 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 State of Formal Methods in Nuclear Control}
 
@@ -109,9 +100,7 @@ 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
+Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. It did not model or verify continuous reactor dynamics.
-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
@@ -191,4 +180,4 @@ This section answered two Heilmeier questions:
 
 \textbf{What are the limits of current practice?} 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.
 
-The economic imperative is clear: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical capability gap is equally clear: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap, establishing what is new and why it will succeed where prior work has not.
+Two imperatives are now clear. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical capability gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap. We establish what is new and why it will succeed where prior work has not.

3-research-approach/v3.tex

@@ -15,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
+Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees of control system behavior. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 a mathematical description of the system. This work draws on
@@ -52,9 +52,25 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty. First, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, continuous modes are classified by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, existing procedural structure is leveraged to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty:
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle.
+\begin{enumerate}
+\item Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally.
+\item Continuous modes are classified by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition.
+\item Existing procedural structure is leveraged to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
+\end{enumerate}
+
+No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+
+\textbf{Why will it succeed?} Three factors ensure practical feasibility:
+
+\begin{enumerate}
+\item Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions.
+\item Mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts.
+\item The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
+\end{enumerate}
+
+We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle.
 
 \begin{figure} 
   \centering
@@ -122,12 +138,7 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 
 The eight-tuple hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
 
-Human control of nuclear power divides into three scopes: strategic,
+Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making for the plant. Objectives at this level are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. These decisions span months or years. The lowest level—the
-operational, and tactical. Strategic control represents high-level,
-long-term decision making for the plant. Objectives at this level are
-complex and economic in scale, such as managing labor needs and supply chains to
-optimize scheduled maintenance and downtime. The time scale at this level is
-long, often spanning months or years. The lowest level—the
 tactical level—controls individual components: pumps, turbines, and
 chemistry. Nuclear power
 plants today have already automated tactical control somewhat; such automation is generally considered ``automatic control.''
@@ -136,9 +147,7 @@ physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
 
-The operational control scope links these two extremes and represents the primary responsibility of human operators
+The operational control scope links these two extremes and represents the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant toward strategic goals—bridging high-level and low-level objectives. 
-today. Operational control takes the current strategic objective and implements
-tactical control objectives to drive the plant toward strategic goals, bridging high-level and low-level goals. 
 
 Consider an example: a strategic goal may be to
 perform refueling at a certain time, while the tactical level of the plant is
@@ -186,22 +195,12 @@ which tactical control law to apply. We target this operational level for autono
 \end{figure}
 
 
-This operational control level is the main reason human
+This operational control level is the main reason human operators are required in nuclear control today. The hybrid nature of this control system makes it difficult to prove a controller will perform according to strategic requirements. Unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the hybrid nature of the system. These operators use prescriptive operating
-operators are required in nuclear control today. The hybrid nature of this control system
-makes it difficult to prove a controller will perform according to
-strategic requirements; unified infrastructure for building and verifying
-hybrid systems does not currently exist. Humans fill this layer
-because their general intelligence provides a safe way to manage
-the hybrid nature of the system. These operators use prescriptive operating
 manuals to perform their control with strict procedures on what control to
 implement at a given time. These procedures are the key to the operational
 control scope.
 
-Constructing a HAHACS leverages two key
+Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe the rules for implementing this control before implementation. A HAHACS's intended behavior must be completely described before construction begins. The
-observations about current practice. First, operational scope control is
-effectively discrete control. Second, operating procedures describe the rules for implementing this control
-before implementation. We must completely describe a HAHACS's intended behavior before
-constructing it. The
 behavior of any control system originates in requirements: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
 these requirements derive from multiple sources including regulatory mandates,
@@ -273,21 +272,13 @@ room for interpretation a weakness that must be addressed.
 
 \subsection{Discrete Controller Synthesis}
 
-With system requirements defined as temporal logic specifications, we now build
+With system requirements defined as temporal logic specifications, we build the discrete control system through reactive synthesis. Reactive synthesis automates the creation of reactive programs from temporal logic specifications.
-the discrete control system through reactive synthesis.
-Reactive synthesis automates the creation of reactive programs from temporal logic specifications.
 A reactive program takes an input for a given state and produces
 an output. Our systems fit this model: the current discrete state and
 status of guard conditions form the input; the next discrete
 state forms the output. 
 
-Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$
+Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ that specifies desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller can exist. This realizability check provides immediate value: an
-that specifies desired system behavior, automatically construct a finite-state
-machine (strategy) that produces outputs in response to environment inputs such
-that all resulting execution traces satisfy $\varphi$. If such a strategy
-exists, the specification is called \emph{realizable}. The synthesis algorithm
-either produces a correct-by-construction controller or reports that no such
-controller can exist. This realizability check provides immediate value: an
 unrealizable specification indicates conflicting or impossible requirements in
 the original procedures, catching errors before implementation. 
 
@@ -314,9 +305,9 @@ algorithms, strategic decisions always follow operating procedures exactly—no
 
 Reactive synthesis produces a provably correct discrete controller from operating procedures. This discrete controller determines when to switch between modes—but hybrid control requires more. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly.
 
-This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
+This subsection describes the continuous control modes that execute within each discrete state. We explain how we verify they satisfy the requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
-This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers can design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -371,10 +362,7 @@ requirements that determine which formal methods tools are appropriate. The foll
 
 Transitory modes move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers.
 
-The control objective for a transitory mode can be stated
+The control objective for a transitory mode can be stated formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
-formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions
-$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop
-dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
 \[
 \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit}
 \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
@@ -554,11 +542,11 @@ outcomes can align best with customer needs.
 
 This section answered two Heilmeier questions:
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates are integrated into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
+\textbf{What is new?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
 
 \textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
 
-Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—the next question becomes: how do we measure success? Section 4 addresses this question by defining Technology Readiness Level advancement as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
+We have now established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation. The next question is: how do we measure success? Section 4 defines Technology Readiness Level advancement as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -4,17 +4,9 @@
 Technology Readiness Levels, progressing from fundamental concepts (TRL 2--3) to validated
 prototype demonstration (TRL 5).
 
-This work begins at TRL 2--3 and aims to reach TRL 5—where
+This work begins at TRL 2--3 and aims to reach TRL 5—where system components operate successfully in a relevant laboratory environment. This section explains why TRL advancement provides the most appropriate success metric. We then define specific criteria for TRL 5.
-system components operate successfully in a relevant laboratory environment.
-This section explains why TRL advancement provides the most appropriate success
-metric and defines specific criteria for TRL 5.
 
-Technology Readiness Levels provide the ideal success metric by
+Technology Readiness Levels provide the ideal success metric by explicitly measuring the gap between academic proof-of-concept and practical deployment—precisely what this work aims to bridge. Academic metrics like papers published or theorems proved cannot capture practical feasibility. Empirical metrics like simulation accuracy or computational speed cannot demonstrate theoretical rigor. Only TRLs measure both simultaneously.
-explicitly measuring the gap between academic proof-of-concept and practical
-deployment—precisely what this work aims to bridge. Academic metrics like
-papers published or theorems proved cannot capture practical feasibility.
-Empirical metrics like simulation accuracy or computational speed cannot
-demonstrate theoretical rigor. TRLs alone measure both simultaneously.
 Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
 progressively demonstrating practical feasibility. Formal verification must
 remain valid as the system moves from individual components to integrated
@@ -89,4 +81,4 @@ a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-This section established how we measure success: TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels despite sound methodology. Section 5 addresses the Heilmeier question \textbf{What could prevent success?} by identifying the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.
+This section answers the Heilmeier question \textbf{How do we measure success?} TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels despite sound methodology. Section 5 addresses the next Heilmeier question: \textbf{What could prevent success?} We identify the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.

5-risks-and-contingencies/v1.tex

@@ -1,10 +1,6 @@
 \section{Risks and Contingencies}
 
-This research relies on several critical assumptions that, if invalidated, require
+This research relies on several critical assumptions that, if invalidated, require scope adjustment or methodological revision. Four primary risks could prevent successful completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration. Each risk has associated early warning indicators and
-scope adjustment or methodological revision. Four primary risks could prevent
-successful completion: computational tractability of
-synthesis and verification, complexity of the discrete-continuous interface,
-completeness of procedure formalization, and hardware-in-the-loop integration. Each risk has associated early warning indicators and
 contingency plans that preserve research value even if core assumptions prove
 false. The staged project structure ensures that partial success yields
 publishable results while clearly identifying remaining barriers to deployment.
@@ -31,8 +27,7 @@ Reachability analysis failing to converge within reasonable time bounds would
 show that continuous mode verification cannot be completed with available
 computational resources.
 
-If computational tractability becomes the limiting factor, we reduce scope to a
+If computational tractability becomes the limiting factor, we reduce scope to a minimal viable startup sequence covering only cold shutdown to criticality to low-power hold. This scope reduction omits power ascension and other operational phases. The reduced sequence still demonstrates the complete methodology—procedure formalization, discrete synthesis, continuous verification, and hardware implementation—while reducing computational burden. The research contribution remains valid: we prove that formal hybrid control synthesis is achievable for safety-critical nuclear applications and clearly identify which operational complexities exceed current computational capabilities. We document the limitation as a scaling constraint requiring future work, not a methodological failure.
-minimal viable startup sequence covering only cold shutdown to criticality to low-power hold, omitting power ascension and other operational phases. This reduced sequence still demonstrates the complete methodology—procedure formalization, discrete synthesis, continuous verification, and hardware implementation—while reducing computational burden. The research contribution remains valid: we prove that formal hybrid control synthesis is achievable for safety-critical nuclear applications and clearly identify which operational complexities exceed current computational capabilities. We document the limitation as a scaling constraint requiring future work, not a methodological failure.
 
 \subsection{Discrete-Continuous Interface Formalization}
 
@@ -148,6 +143,6 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-This section addressed the Heilmeier question: \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid: partial success yields publishable results that clearly identify remaining barriers to deployment.
+This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid. Partial success yields publishable results that clearly identify remaining barriers to deployment.
 
-With technical feasibility established through the methodology (Section 3), success metrics defined (Section 4), and risks addressed with contingency plans (Section 5), the research plan is complete from a technical perspective. Section 6 now addresses the remaining Heilmeier questions that establish broader impact: \textbf{Who cares?} \textbf{Why now?} \textbf{What difference will it make?}
+We have now established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (Section 5). The research plan is complete from a technical perspective. Section 6 addresses the remaining Heilmeier questions that establish broader impact: \textbf{Who cares? Why now? What difference will it make?}

6-broader-impacts/v1.tex

@@ -10,12 +10,7 @@ Deploying SMRs at datacenter sites minimizes transmission losses and
 eliminates emissions. However, nuclear power
 economics at this scale demand careful attention to operating costs.
 
-The U.S. Energy Information Administration's Annual Energy Outlook
+The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. Within this
-2022 projects advanced nuclear power entering service in 2027 will cost
-\$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is
-projected to reach 1,050 terawatt-hours annually by
-2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would
-generate total annual costs exceeding \$92 billion. Within this
 figure, operations and maintenance represents a substantial component. The EIA
 estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour,
 with additional variable O\&M costs embedded in fuel and operating
@@ -27,9 +22,7 @@ to \$21--28 billion annually for projected datacenter demand.
 \$21--28 billion annual O\&M cost challenge through high-assurance autonomous
 control, making small modular reactors economically viable for datacenter power.
 
-Current nuclear operations require full control room staffing for each
+Current nuclear operations require full control room staffing for each reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output. This makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
-reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making per-megawatt costs prohibitive. These staffing requirements drive the economic challenge
-that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
 specifications automates routine operational sequences that currently require
 constant human oversight. This enables a fundamental shift from direct operator
 control to supervisory monitoring, where operators oversee multiple autonomous
@@ -77,8 +70,8 @@ This section answered three Heilmeier questions:
 
 \textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control.
 
-\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent, and formal methods tools have matured to the point where compositional hybrid verification is achievable. 
+\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent. Formal methods tools have matured to the point where compositional hybrid verification is achievable.
 
-\textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
+\textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier. It also establishes a generalizable framework for safety-critical autonomous systems.
 
-Section 8 addresses the final Heilmeier question—how long will it take?—presenting a structured 24-month research plan with milestones tied to Technology Readiness Level advancement.
+Section 8 addresses the final Heilmeier question: \textbf{How long will it take?} We present a structured 24-month research plan with milestones tied to Technology Readiness Level advancement.