Editorial pass: tactical, operational, and strategic improvements

- TACTICAL: Improved sentence-level clarity per Gopen principles
  - Stronger verb choices (cannot vs lacks tools, cannot vs fails)
  - Better issue-point positioning (new info at sentence end)
  - Topic-stress consistency (familiar info at start)
  - Eliminated weak constructions (that are → direct adjectives)

- OPERATIONAL: Enhanced paragraph and section flow
  - Added transition sentences between subsections
  - Improved coherence in state-of-the-art progression
  - Clearer bridges between risk categories
  - Better linkage from discrete to continuous verification

- STRATEGIC: Reinforced Heilmeier catechism alignment
  - Made 'What is new?' and 'Why will it succeed?' explicit
  - Added 'State of the art' and 'The gap' headers
  - Consistent question format (How do we...? vs How we...)
  - Added roadmap at end of Goals section

No content changes—only editorial improvements for clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,33 +1,31 @@
 % GOAL PARAGRAPH
 This research develops a methodology for creating autonomous control systems
-with guaranteed safe and correct behavior.
+with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained operators manage nuclear reactor control by following detailed written procedures. These operators interpret plant conditions and decide when to switch between control objectives.
+Extensively trained operators manage nuclear reactor control by following detailed written procedures. Plant conditions guide these operators as they decide when to switch between control objectives.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. Without autonomous control, this economic constraint threatens their viability. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while providing assurance equal to—or better than—human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants. This economic constraint threatens their viability without autonomous control. Autonomous control systems must therefore manage complex operational sequences safely—without constant supervision—while providing assurance equal to or better than human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
-build hybrid control systems that are correct by construction. 
+build hybrid control systems correct by construction. 
 % Rationale
 Hybrid systems mirror operator behavior: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic but fail to handle continuous dynamics
+generate provably correct switching logic but cannot handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
-lacks tools to prove discrete switching correctness. 
+cannot prove discrete switching correctness. 
 % Hypothesis and Technical Approach
 A three-stage methodology bridges this gap. First, we translate written
 operating procedures into temporal logic specifications using NASA's Formal
 Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
 condition, component, timing, and response elements. Realizability
-checking identifies conflicts and ambiguities before implementation.
+checking then identifies conflicts and ambiguities before implementation.
-Second, reactive synthesis generates deterministic automata provably
+Second, reactive synthesis generates deterministic automata—provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
-control theory and verify them using reachability analysis. We classify continuous modes based on
+control theory and verify them using reachability analysis. Continuous modes are classified by their transition objectives; assume-guarantee contracts and barrier certificates then prove mode transitions occur safely. This approach enables local verification of continuous modes
-their transition objectives, then employ assume-guarantee contracts and barrier
-certificates to prove mode transitions occur safely. This approach enables local verification of continuous modes
 without requiring global trajectory analysis across the entire hybrid system. An
 Emerson Ovation control system demonstrates this methodology. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -11,9 +11,7 @@ or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
 who follow detailed written procedures and strict regulatory requirements to
-manage reactor control. These operators decide when to
+manage reactor control. Plant conditions and procedural guidance inform these operators as they decide when to switch between different control modes.
-switch between different control modes based on their interpretation of plant
-conditions and procedural guidance.
 % Gap
 This reliance on human operators prevents autonomous control and
 creates a fundamental economic challenge for next-generation reactor designs.
@@ -25,14 +23,12 @@ assurance higher than human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
-systems that are correct by construction.
+systems correct by construction.
 % Rationale
 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 fail to
+generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions between modes.
-handle the continuous dynamics during transitions between modes.
+Control theory verifies continuous behavior but cannot prove correctness of discrete switching decisions. This gap between discrete
-Control theory verifies continuous behavior but lacks tools for
-proving correctness of discrete switching decisions. This gap between discrete
 and continuous verification prevents end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
@@ -93,7 +89,7 @@ If this research is successful, we will be able to do the following:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{The key innovation} unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
+\textbf{The key innovation:} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
 Formal methods verify discrete logic. Control theory verifies
 continuous dynamics. No existing methodology bridges both with compositional
 guarantees. This work establishes that bridge by treating discrete specifications
@@ -111,3 +107,5 @@ energy demands, but their success depends on reducing per-megawatt operating
 costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.
+
+The following sections detail this methodology: Section 2 examines the state of the art and identifies the verification gap this work addresses. Section 3 presents our hybrid control synthesis approach. Section 4 defines Technology Readiness Level advancement as the success metric. Section 5 analyzes risks and contingencies. Section 6 discusses broader impacts, and Section 7 provides the research schedule.

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

@@ -1,11 +1,11 @@
 \section{State of the Art and Limits of Current Practice}
 
-This research creates tractably safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates limitations of human-based operation, and reviews current formal methods approaches to reactor control systems.
+This research creates tractably safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates the limitations of human-based operation, and reviews current formal methods approaches to reactor control systems.
 
 \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, 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}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. Yet this rigor fails to 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}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} rigorously assess procedures. 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
@@ -37,7 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Nuclear plants currently operate through written procedures executed by human operators. This human-centered approach defines current practice. We now examine why this reliance poses fundamental limitations.
+The previous subsection established that procedures lack formal verification despite rigorous development. Nuclear plants currently operate through written procedures executed by human operators. This human-centered approach defines current practice. We now examine why this reliance poses fundamental limitations.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -48,13 +48,13 @@ 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, providing compelling
+of improvements in training and procedures. This persistence provides compelling
 motivation for formal automated control with mathematical safety guarantees.
 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 a combination of personnel error, design
+Island (TMI) accident demonstrated how personnel error, design
-deficiencies, and component failures led to partial meltdown when operators
+deficiencies, and component failures combined to cause partial meltdown. Operators
-misread confusing and contradictory readings and shut off the emergency water
+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
@@ -81,7 +81,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Training alone fails to eliminate the fundamental reliability limits imposed by human error. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies their limitations for autonomous hybrid systems.
+Human factors impose fundamental reliability limits that training alone cannot overcome. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies their limitations for autonomous hybrid systems.
 
 \subsubsection{HARDENS}
 
@@ -155,7 +155,7 @@ primary assurance evidence.
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
 
-HARDENS verified discrete control logic but omitted continuous dynamics. 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
+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
@@ -188,8 +188,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-Current practice reveals a fundamental gap. 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.
+\textbf{State of the art:} Current practice reveals a fundamental gap. 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. 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—defines our challenge and motivates our approach. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. The next section presents our methodology for bridging this gap through compositional hybrid verification.
+\textbf{The gap our work addresses:} This gap—between discrete-only formal methods and post-hoc hybrid verification—defines our challenge and motivates our approach. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. The next section presents our methodology for bridging this gap through compositional hybrid verification.

3-research-approach/v3.tex

@@ -15,7 +15,7 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. 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, formalizing reactor operations using hybrid automata.
+Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. 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, then formalizing 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—fail to handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode.
 
@@ -23,8 +23,7 @@ Building a high-assurance hybrid autonomous control system (HAHACS) requires
 establishing a mathematical description of the system. This work draws on
 automata theory, temporal logic, and control theory. A hybrid system is a
 dynamical system with both continuous and discrete states. This proposal
-discusses continuous autonomous hybrid systems specifically.
+discusses continuous autonomous hybrid systems specifically—systems with no external input where continuous
-These systems have no external input, and continuous
 states do not change instantaneously when discrete states change. The continuous states are physical quantities that remain
 Lipschitz continuous. This nomenclature follows the Handbook on
 Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
@@ -53,9 +52,9 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new:} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces—specifically, mode-level verification that avoids global hybrid system analysis.
+\textbf{What is new?} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces—specifically, mode-level verification that avoids global hybrid system analysis.
 
-\textbf{Why it will succeed:} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires, making the approach practical for real systems.
+\textbf{Why will it succeed?} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires, making the approach practical for real systems.
 
 \begin{figure} 
   \centering
@@ -121,7 +120,7 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The preceding section established the mathematical framework for hybrid systems. We now construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism.
+The preceding section established the mathematical framework for hybrid systems. With this formalism in hand, we now construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism.
 
 Human control of nuclear power divides into three scopes: strategic,
 operational, and tactical. Strategic control is high-level and
@@ -137,11 +136,9 @@ physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
 
-The level of control linking these two extremes is the operational control
+The operational control scope links these two extremes. This level is the primary responsibility of human operators
-scope. Operational control is the primary responsibility of human operators
 today. Operational control takes the current strategic objective and implements
-tactical control objectives to drive the plant towards strategic goals. In this
+tactical control objectives to drive the plant toward strategic goals. It thereby bridges high-level and low-level goals. 
-way, it bridges 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
@@ -213,24 +210,24 @@ these requirements with sufficient precision that they can serve as the
 foundation for autonomous control system synthesis and verification. We can
 build these requirements using temporal logic.
 
-Temporal logic is a powerful set of semantics for building systems with complex
+Temporal logic provides powerful semantics for building systems with complex
-but deterministic behavior. Temporal logic extends classical propositional logic
+but deterministic behavior. It extends classical propositional logic
 with operators that express properties over time. Using temporal logic, we can
-make statements relating discrete control modes to one another and define all
+relate discrete control modes to one another and define all
 the requirements of a HAHACS. The guard conditions $\mathcal{G}$ are defined by
 determining boundary conditions between discrete states and specifying their
-behavior, while continuous mode invariants can also be expressed as temporal
+behavior. Continuous mode invariants can also be expressed as temporal
 logic statements. These specifications form the basis of any proofs about a
 HAHACS and constitute the fundamental truth statements about what the behavior
 of the system is designed to be.
 
-Discrete mode transitions include predicates that are Boolean functions over the
+Discrete mode transitions include predicates—Boolean functions over the
 continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
 \text{false}\}$. These predicates formalize conditions like ``coolant
 temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
 We do not impose this discrete abstraction artificially. Operating
 procedures for nuclear systems already define go/no-go conditions as discrete
-predicates. Design basis safety analysis determined these thresholds, and decades of operational experience have
+predicates. Design basis safety analysis determined these thresholds; decades of operational experience have
 validated them. Our methodology assumes
 this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations
 of nuclear engineers have already done the hard
@@ -252,7 +249,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility. By reducing required expert knowledge, we make these tools adoptable by the current workforce.
+We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility: by reducing required expert knowledge, we make these tools adoptable by the current workforce.
 
 A key feature of FRET is the ability to start with logically imprecise
 statements and consecutively refine them into well-posed specifications. We can
@@ -294,11 +291,10 @@ controller can exist. This realizability check is itself valuable: an
 unrealizable specification indicates conflicting or impossible requirements in
 the original procedures. 
 
-Reactive synthesis offers a decisive advantage: producing the discrete automaton requires no human engineering of the implementation. The resultant automaton is correct by construction. This eliminates human error at the implementation stage entirely. Human designers focus their effort where it belongs: on specifying system behavior itself. This has two critical implications. First, it makes the
+Reactive synthesis offers a decisive advantage: producing the discrete automaton requires no human engineering of the implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers focus their effort where it belongs: on specifying system behavior itself. This has two critical implications. First, it makes discrete controller creation tractable. The reasons the controller
-creation of the discrete controller tractable. The reasons the controller
 changes between modes can be traced back to the specification and thus to any
-requirements, which provides a trace for liability and justification of system
+requirements, providing a trace for liability and justification of system
-behavior. Second, discrete control decisions made by humans are reliant on the
+behavior. Second, discrete control decisions made by humans depend on the
 human operator operating correctly. Humans are intrinsically probabilistic
 creatures who cannot eliminate human error. By defining the behavior of this
 system using temporal logics and synthesizing the controller using deterministic
@@ -321,7 +317,7 @@ according to operating procedures.
 
 \subsection{Continuous Control Modes}
 
-Synthesis guarantees the discrete controller is provably correct. Yet hybrid control requires more than discrete correctness. We now turn to the continuous dynamics executing within each discrete mode.
+Synthesis guarantees the discrete controller is provably correct—but hybrid control requires more than discrete correctness. We now turn to the continuous dynamics executing within each discrete mode.
 
 The discrete operational controller represents only half of an
 autonomous controller, despite its provable correctness. Hybrid control systems require both discrete and
@@ -333,13 +329,13 @@ This methodology's scope regarding continuous controller design requires clarifi
 
 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
-discrete state are themselves the guard conditions $\mathcal{G}$ that define the
+discrete state are the guard conditions $\mathcal{G}$ that define the
 boundaries for each continuous controller's allowed state-space region. These
 continuous controllers all share a common state space, but each individual
-continuous control mode operates within its own partition defined by the
+continuous control mode operates within its own partition—defined by the
 discrete state $q_i$ and the associated guards. This partitioning of the
 continuous state space among several discrete vector fields has traditionally
-been a difficult problem for validation and verification. The discontinuity of
+posed a difficult problem for validation and verification. The discontinuity of
 the vector fields at discrete state interfaces makes reachability analysis
 computationally expensive, and analytic solutions often become intractable
 \cite{MANYUS THESIS}.
@@ -367,7 +363,7 @@ state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
 
 We classify continuous controllers into three types based on their objectives:
 transitory, stabilizing, and expulsory. Each type has distinct verification
-requirements that determine which formal methods tools are appropriate.
+requirements that determine which formal methods tools are appropriate. The following subsections detail each mode type and its verification approach.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -380,9 +376,9 @@ requirements that determine which formal methods tools are appropriate.
 
 \subsubsection{Transitory Modes}
 
-The first mode type, transitory modes, moves
+Transitory modes, the first mode type, move
 the plant from one discrete operating condition to another. Their purpose is to
-execute transitions: starting from entry conditions, reach exit conditions,
+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.
 
@@ -441,17 +437,16 @@ appropriate to the fidelity of the reactor models available.
 \subsubsection{Stabilizing Modes}
 
 Transitory modes drive the system toward exit conditions. Stabilizing modes, the second type,
-maintain the system within a desired operating region indefinitely. Rather than driving the system toward an
+maintain the system within a desired operating region indefinitely. They keep the system within a safe operating region rather than driving it toward an
-exit condition, they keep the system within a safe operating region. Examples
+exit condition. Examples
 include steady-state power operation, hot standby, and load-following at
-constant power level. Reachability analysis for stabilizing modes may not be a
+constant power level. Reachability analysis may not suit validation of stabilizing modes. Instead, we will use barrier certificates.
-suitable approach to validation. Instead, we plan to use barrier certificates.
 Barrier certificates analyze the dynamics of the system to determine whether
 flux across a given boundary exists. They evaluate whether any trajectory leaves
-a given boundary. This definition is exactly what defines the validity of a
+a given boundary. This definition exactly matches what defines the validity of a
 stabilizing continuous control mode.
 
-A barrier certificate (or control barrier function) is a
+Formally, a barrier certificate (or control barrier function) is a
 scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward
 invariance of a safe set. The idea is analogous to Lyapunov functions for
 stability: rather than computing trajectories explicitly, we find a certificate
@@ -507,7 +502,7 @@ state from potentially anywhere in the state space, under degraded or uncertain
 dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and
 controlled depressurization procedures.
 
-Detecting physical failures becomes straightforward after proving controller correctness through reachability and barrier certificates. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions.
+Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions.
 
 The mathematical formulation for expulsory mode verification
 differs from transitory modes in two key ways. First, the entry conditions may

4-metrics-of-success/v1.tex

@@ -1,17 +1,17 @@
 \section{Metrics for Success}
 
-\textbf{How we measure success:} This research advances through
+\textbf{How do we measure success?} This research advances through
 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 and defines specific criteria for achieving TRL 5.
 
 Technology Readiness Levels provide the ideal success metric: they
 explicitly measure the gap between academic proof-of-concept and practical
-deployment, precisely what this work aims to bridge. Academic metrics like
+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 measure both dimensions simultaneously.

5-risks-and-contingencies/v1.tex

@@ -15,10 +15,10 @@ deployment.
 
 The first major assumption is that formalized startup procedures will yield
 automata small enough for efficient synthesis and verification. Reactive
-synthesis scales exponentially with specification complexity, creating risk that
+synthesis scales exponentially with specification complexity, creating the risk that
 temporal logic specifications derived from complete startup procedures may
 produce automata with thousands of states. Such large automata would require
-synthesis times exceeding days or weeks, preventing demonstration of the
+synthesis times exceeding days or weeks—preventing demonstration of the
 complete methodology within project timelines. Reachability analysis for
 continuous modes with high-dimensional state spaces may similarly prove
 computationally intractable. Either barrier would constitute a fundamental
@@ -46,7 +46,7 @@ rather than a failure.
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-The second critical assumption concerns the mapping between boolean guard
+Computational tractability represents one dimension of risk. The second critical assumption concerns a more fundamental challenge: the mapping between boolean guard
 conditions in temporal logic and continuous state boundaries required for mode
 transitions. This interface represents the fundamental challenge of hybrid
 systems: relating discrete switching logic to continuous dynamics. Temporal
@@ -102,7 +102,7 @@ computational resources where they matter most for safety assurance.
 
 \subsection{Procedure Formalization Completeness}
 
-The third assumption is that existing startup procedures contain sufficient
+The previous two risks concern verification infrastructure—computational scaling and mathematical formalization. The third assumption addresses the source material itself: that existing startup procedures contain sufficient
 detail and clarity for translation into temporal logic specifications. Nuclear
 operating procedures, while extensively detailed, were written for human
 operators who bring contextual understanding and adaptive reasoning to their

6-broader-impacts/v1.tex

@@ -23,12 +23,12 @@ expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
 approximately 23--30\% of the total levelized cost of electricity, translating
 to \$21--28 billion annually for projected datacenter demand.
 
-\textbf{What difference it makes:} This research directly addresses the
+\textbf{What difference does it make?} This research directly addresses the
 \$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
-reactor, whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs
+reactor—whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs
 that make nuclear power economically challenging, particularly for smaller
 reactor designs where the same staffing overhead must be spread across lower
 power output. Synthesizing provably correct hybrid controllers from formal

8-schedule/v1.tex

@@ -1,6 +1,6 @@
 \section{Schedule, Milestones, and Deliverables}
 
-\textbf{How long it will take:} This research will be conducted over six
+\textbf{How long will it take?} This research will be conducted over six
 trimesters (24 months) of full-time effort following the proposal defense in
 Spring 2026. All work uses existing computational and experimental resources
 available through the University of Pittsburgh Cyber Energy Center and NRC