Multi-pass editorial review: tactical, operational, and strategic improvements

TACTICAL (sentence-level):
- Strengthened verb choices (fail/prove vs. cannot/can)
- Removed weak constructions (can be/may be → is/are)
- Improved topic-stress positioning
- Enhanced parallel structure in lists
- Tightened passive constructions where appropriate

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Strengthened flow from transitory → stabilizing → expulsory modes
- Enhanced coherence in formal methods discussion
- Better linkage between HARDENS and dL subsections
- Clearer progression in continuous controller classification

STRATEGIC (document-level):
- Sharpened Heilmeier question answers throughout
- Improved section-to-section linkages
- Strengthened research contribution clarity
- Enhanced motivation for methodology choices
- Better alignment of conclusions with next section openings

1-goals-and-outcomes/research_statement_v1.tex

@@ -10,21 +10,21 @@ Small modular reactors face a fundamental economic challenge: per-megawatt staff
 We combine formal methods from computer science with control theory to
 build hybrid control systems that are correct by construction. 
 % Rationale
-Hybrid systems mirror how operators work: discrete
+Hybrid systems mirror operator decision-making: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic but cannot handle continuous dynamics
+generate provably correct switching logic but fail to handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
-cannot prove the correctness of discrete switching decisions. 
+fails to prove discrete switching correctness. 
 % Hypothesis and Technical Approach
-Our methodology bridges this gap through three stages. First, we translate written
+Three stages bridge 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.
-Second, reactive synthesis generates deterministic automata that are 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 by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
+control theory and verify them through reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
 without requiring global trajectory analysis across the entire hybrid system. We demonstrate this methodology on an
 Emerson Ovation control system. 
 % Pay-off

1-goals-and-outcomes/v1.tex

@@ -10,17 +10,17 @@ 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. Plant conditions and procedural guidance inform operator decisions when they switch between different control modes.
 % Gap
-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.
+Human operator reliance prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding 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.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control systems that are 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 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.
 % Hypothesis
-Our approach closes this gap by synthesizing discrete mode transitions directly
+This approach closes the gap by synthesizing discrete mode transitions directly
 from written operating procedures and verifying continuous behavior between
 transitions. We formalize existing procedures into logical
-specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers provably free from design
+specifications and verify continuous dynamics against transition requirements. This produces autonomous controllers provably free from design
 defects. The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring that solutions developed here align with practical implementation
 requirements.
 
@@ -76,7 +76,7 @@ These three outcomes—procedure translation, continuous verification, and hardw
 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
-as contracts that continuous controllers must satisfy, enabling independent
+as contracts that continuous controllers must satisfy. This enables independent
 verification of each layer while guaranteeing correct composition.
 
 % Outcome Impact

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

@@ -4,7 +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. 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}. Developers rely 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.
+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. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Developers rely 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 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.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -36,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 independent of procedure quality. 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, but this represents only half the reliability challenge. The second pillar of current practice—human operators executing these procedures—introduces additional reliability limitations independent of procedure quality. Procedures define what to do. Human operators determine when and how to apply them. Even perfect procedures fail to 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
@@ -71,7 +71,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Two limitations emerge from current practice: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach by providing 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 emerge from current practice: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. Yet as this subsection demonstrates, even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems.
 
 \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 
@@ -141,7 +141,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Recognizing this gap, 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
+While HARDENS verified discrete control logic without continuous dynamics, other researchers attacked the problem from the opposite direction: 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
@@ -176,8 +176,8 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section establishes the current state of practice by answering two Heilmeier questions:
 
-\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and does not scale to system synthesis.
+\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis.
 
 \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.
 
-Two imperatives emerge from this analysis. First, the economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, 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, establishing what is new and why it will succeed where prior work has not.
+Two imperatives emerge. First, the economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, the technical gap: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 bridges this gap, establishing what is new and why it succeeds where prior work failed.

3-research-approach/v3.tex

@@ -15,16 +15,16 @@
 % ----------------------------------------------------------------------------
 % 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, formalizing reactor operations using hybrid automata.
+Previous approaches 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, formalizing reactor operations as 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 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.
+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 fail to 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
 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: systems with no external input where continuous
-states do not change instantaneously when discrete states change. These continuous states represent physical quantities that remain
+addresses continuous autonomous hybrid systems specifically: systems with no external input where continuous
+states remain continuous when discrete states change. These continuous states represent physical quantities that remain
 Lipschitz continuous. We follow the nomenclature from the Handbook on
 Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
 for convenience:
@@ -52,12 +52,12 @@ where:
 
 Creating a HAHACS requires constructing this tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution lies in the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty:
+\textbf{What is new in this research?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty:
 
 \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.
+\item Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of global hybrid system verification.
+\item Continuous modes classify by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition.
+\item Existing procedural structure avoids global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
 No prior work integrates these three techniques into a systematic design methodology spanning procedures to verified implementation.
@@ -66,11 +66,11 @@ No prior work integrates these three techniques into a systematic design methodo
 
 \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 Mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, bounding computational complexity 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.
+We demonstrate feasibility on production control systems with realistic reactor models, not merely in principle.
 
 \begin{figure} 
   \centering
@@ -147,7 +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 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. 
+The operational control scope links these two extremes and represents the primary responsibility of human operators today. Operational control takes strategic objectives and implements tactical control sequences to achieve them, bridging high-level goals with low-level execution. 
 
 Consider an example: a strategic goal may be to
 perform refueling at a certain time, while the tactical level of the plant is
@@ -247,7 +247,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: reducing required expert knowledge makes these tools adoptable by the current workforce.
+We 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 proves crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current workforce.
 
 FRET's key feature is its ability to start with logically imprecise
 statements and consecutively refine them into well-posed specifications. We can
@@ -306,7 +306,7 @@ Reactive synthesis produces a provably correct discrete controller from operatin
 
 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 design continuous controllers using standard control theory techniques. Our contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope 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 provides the verification framework confirming that 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
@@ -345,8 +345,8 @@ $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
 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. The following subsections detail each mode type and its verification approach.
+transitory, stabilizing, and expulsory. Each type requires distinct verification
+tools matched to its control objective. Transitory modes drive the plant between operating conditions. Stabilizing modes maintain the plant within operating regions. Expulsory modes ensure safety under degraded conditions. The following subsections detail each mode type and its verification approach.
 
 %%% NOTES (Section 4):
 % - Add figure showing the relationship between entry/exit/safety sets
@@ -410,7 +410,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-While transitory modes drive the system toward exit conditions, stabilizing modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach. Reachability analysis answers "can the system reach a target?" while stabilizing modes must instead prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool for this question.
+Transitory modes drive the system toward exit conditions. Stabilizing modes do the opposite: they maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach. Reachability analysis answers "can the system reach a target?" Stabilizing modes ask instead "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
 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 exactly matches what defines the validity of a
@@ -462,7 +462,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations under the assumption that plant dynamics match the design model. When the plant deviates from expected behavior—through component failures, sensor degradation, or unanticipated disturbances—expulsory modes ensure safety. These continuous controllers prioritize robustness over optimality. The control objective is to drive the plant to a safe shutdown 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.
+Transitory and stabilizing modes handle nominal operations where plant dynamics match the design model. Expulsory modes handle the opposite case: when the plant deviates from expected behavior through component failures, sensor degradation, or unanticipated disturbances. These continuous controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown 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.
 
 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.
 
@@ -545,7 +545,7 @@ This section establishes the methodology by answering two Heilmeier questions:
 
 \textbf{Why will this approach succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, so 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.
 
-We have now established the complete methodology from procedure formalization through discrete synthesis to continuous verification and hardware implementation. Section 4 addresses the next Heilmeier question: how do we measure success? Technology Readiness Level advancement serves as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
+The complete methodology now spans from procedure formalization through discrete synthesis to continuous verification and hardware implementation. But establishing what we will do and why it will work leaves a critical question unanswered: how do we measure success? Section 4 addresses this through Technology Readiness Level advancement, 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

@@ -6,7 +6,7 @@ prototype demonstration (TRL 5).
 
 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 first explains why TRL advancement provides the most appropriate success metric, then defines specific criteria for each level from TRL 3 through TRL 5.
 
-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 fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. Only TRLs measure both simultaneously.
+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 bridges. Academic metrics like papers published or theorems proved fail to capture practical feasibility. Empirical metrics like simulation accuracy or computational speed fail to demonstrate theoretical rigor. Only TRLs 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

5-risks-and-contingencies/v1.tex

@@ -1,6 +1,6 @@
 \section{Risks and Contingencies}
 
-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
+Every research plan rests on assumptions. When those assumptions prove false, the research must adapt. 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.
@@ -143,6 +143,6 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-This section identifies barriers to success by answering 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, with even partial success yielding publishable results that clearly identify remaining barriers to deployment.
+This section identifies barriers to success by answering 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, with partial success yielding publishable results that clearly identify remaining barriers to deployment.
 
-The research plan is now complete from a technical perspective: we have established technical feasibility through the methodology (Section 3), defined success metrics (Section 4), and addressed risks with contingency plans (this section). Section 6 completes the Heilmeier framework by establishing broader impact: \textbf{Who cares? Why now? What difference will it make?}
+The research plan is now complete from a technical perspective: we have established what we will do (Section 3), how we measure success (Section 4), and what might prevent it (this section). The final Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 establishes broader impact by connecting this technical methodology to urgent economic and infrastructure challenges.

6-broader-impacts/v1.tex

@@ -10,8 +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 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
+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. Operations and maintenance represents a substantial component of this figure. 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
 expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
@@ -70,8 +69,8 @@ This section establishes impact by answering three Heilmeier questions:
 
 \textbf{Who cares?} The nuclear industry, datacenter operators, and any organization facing high operating costs from staffing-intensive safety-critical control.
 
-\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent, while formal methods tools have matured to where compositional hybrid verification has become achievable.
+\textbf{Why now?} AI infrastructure demands have made nuclear economics urgent. Formal methods tools have matured to where compositional hybrid verification has become 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.
 
-Section 8 completes the Heilmeier framework by addressing the final question: \textbf{How long will it take?} A structured 24-month research plan progresses through milestones tied to Technology Readiness Level advancement.
+One question remains: \textbf{How long will it take?} Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement.