Editorial pass: Tactical/Operational/Strategic improvements

TACTICAL (sentence-level):
- Strengthened topic-stress positioning
- Converted passive to active voice where appropriate
- Improved verb choices
- Enhanced topic strings for continuity
- Replaced 'we' with 'this work' for consistency

OPERATIONAL (paragraph/section):
- Improved transitions between subsections
- Added paragraph breaks for better flow
- Strengthened coherence in mode classification sections
- Enhanced transition from HARDENS to dL discussion

STRATEGIC (document-level):
- Verified Heilmeier alignment throughout
- Strengthened section transitions
- Improved signposting of what each section answers
- Enhanced linkage between State of Art and Research Approach

1-goals-and-outcomes/research_statement_v1.tex

@@ -7,11 +7,11 @@ Nuclear reactors require extensively trained operators who follow detailed writt
 Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. These reactors need autonomous control systems that safely manage complex operational sequences without constant supervision—systems that provide assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-Formal methods from computer science combine with control theory to build hybrid control systems correct by construction. 
+This research combines formal methods from computer science with control theory to build hybrid control systems correct by construction. 
 % Rationale
-Hybrid systems mirror operator decision-making: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when transitions involve continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 
+Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. 
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET), which structures requirements into scope, condition, component, timing, and response elements. Realizability checking identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata—provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode, then reachability analysis verifies them. Continuous modes classify by transition objectives. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification of continuous modes without global trajectory analysis across the entire hybrid system. An Emerson Ovation control system demonstrates the methodology. 
+Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET), which structures requirements into scope, condition, component, timing, and response. Realizability checking identifies conflicts and ambiguities before implementation. Second, reactive synthesis generates deterministic automata—provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode, which reachability analysis then verifies. Continuous modes classify by transition objectives: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. An Emerson Ovation control system demonstrates the methodology. 
 % Pay-off
 This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -11,11 +11,11 @@ Nuclear plant operations rely on extensively trained human operators who follow
 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 far exceeding those of conventional plants, threatening economic viability. The nuclear industry needs autonomous control systems that safely manage complex operational sequences without constant human supervision—systems that provide assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-Formal methods combine with control theory to build hybrid control systems correct by construction.
+This research combines formal methods with control theory to build hybrid control 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 when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach provides end-to-end correctness guarantees.
+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 when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. No existing approach provides end-to-end correctness guarantees for both layers.
 % Hypothesis
-This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Existing procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
+This approach closes the gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. Operating procedures formalize into logical specifications; continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation
 requirements.

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. 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 drive development, 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 confirms 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}. Expert judgment and simulator validation drive development—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 confirms 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
@@ -21,7 +21,7 @@ The division between automated and human-controlled functions reveals the fundam
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development—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. Even perfect 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 executing these procedures—introduces reliability limitations independent of procedure quality. Procedures define what to do; human operators determine when and how. Even perfect 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
@@ -56,7 +56,7 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
+Current practice reveals two critical limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Formal methods offer an alternative—mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. 
 
 Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. Two approaches illustrate this gap: HARDENS verified discrete logic without continuous dynamics, while differential dynamic logic handles hybrid verification only post-hoc. The following subsections examine each approach and its limitations.
 
@@ -121,7 +121,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-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
+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 complementary approach 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
@@ -160,4 +160,4 @@ This section establishes the current state of practice by answering two Heilmeie
 
 \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. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical imperative: current approaches verify either discrete logic or continuous dynamics, never both compositionally. These limitations define the research opportunity. Section 3 bridges this gap by establishing what makes this approach new and why it will succeed where prior work has failed.
+Two imperatives emerge from these limitations. The economic imperative: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical imperative: current approaches verify either discrete logic or continuous dynamics—never both compositionally. These limitations define the research opportunity. Section 3 bridges this gap by establishing what makes this approach new and why it will succeed where prior work has failed.

3-research-approach/v3.tex

@@ -15,17 +15,17 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-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 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.
+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 despite consuming enormous resources. This work bridges the 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 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; continuous controllers govern plant behavior within each mode.
 
-Building a high-assurance hybrid autonomous control system (HAHACS) requires
+Building a high-assurance hybrid autonomous control system requires
 a mathematical description of the system. This work draws on
 automata theory, temporal logic, and control theory to provide that description. A hybrid system is a
 dynamical system with both continuous and discrete states. This proposal
 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
+Lipschitz continuous. This work follows the nomenclature from the Handbook on
 Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here
 for convenience:
 
@@ -52,11 +52,11 @@ 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?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics, never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. This work composes them into a complete methodology for hybrid control synthesis through three key innovations:
+\textbf{What is new in this research?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. This work composes them into a complete methodology for hybrid control synthesis through three key innovations:
 
 \begin{enumerate}
 \item \textbf{Contract-based decomposition:} Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of global hybrid system verification.
-\item \textbf{Mode classification:} Continuous modes classify by objective (transitory, stabilizing, expulsory), selecting appropriate verification tools and enabling mode-local analysis with provable composition.
+\item \textbf{Mode classification:} Continuous modes classify by objective (transitory, stabilizing, expulsory), which selects appropriate verification tools and enables mode-local analysis with provable composition.
 \item \textbf{Procedure-driven structure:} Existing procedural structure avoids global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
@@ -65,12 +65,12 @@ No prior work integrates these three techniques into a systematic design methodo
 \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 Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—this work formalizes existing structure rather than imposing artificial abstractions.
 \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 in principle. Figure~\ref{fig:hybrid_automaton} illustrates this hybrid structure for a simplified reactor startup sequence.
+This work demonstrates feasibility on production control systems with realistic reactor models, not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
 
 \begin{figure} 
   \centering
@@ -246,7 +246,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-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.
+This work uses 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 nuclear 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 executing within each discrete state and explains how they verify against 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 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.
+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. This work assumes engineers design continuous controllers using standard control theory techniques. The 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
@@ -410,7 +410,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-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.
+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 +464,9 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-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.
+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.
 
@@ -539,13 +543,13 @@ of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-This section answers two critical Heilmeier questions:
+This section establishes the research approach by answering two critical Heilmeier questions:
 
-\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. Three innovations distinguish this approach: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion.
+\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations distinguish this approach: using discrete synthesis to define verification contracts (inverting traditional global analysis), classifying continuous modes by objective to select appropriate verification tools, and leveraging existing procedural structure to avoid intractable state explosion.
 
 \textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the approach formalizes existing structure rather than imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility.
 
-The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. One critical question remains: \textit{how will success be measured?} Section 4 addresses this through Technology Readiness Level advancement, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation (TRL 3) through integrated simulation (TRL 4) to hardware-in-the-loop testing (TRL 5).
+The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. Sections 2 and 3 have established what has been done, what is new, and why it will succeed. One critical question remains: \textit{How will success be measured?} Section 4 addresses this through Technology Readiness Level advancement, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation (TRL 3) through integrated simulation (TRL 4) to hardware-in-the-loop testing (TRL 5).
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -4,11 +4,9 @@
 
 This work begins at TRL 2--3 and aims to reach TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric for this work, bridging the gap between academic proof-of-concept and practical deployment. This section explains why, 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 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.
+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. TRLs measure both simultaneously.
-Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
+
-progressively demonstrating practical feasibility. Formal verification must
+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 hardware testing.
-remain valid as the system moves from individual components to integrated
-hardware testing.
 
 The nuclear industry requires extremely high assurance before deploying new
 control technologies. Demonstrating theoretical correctness alone proves

5-risks-and-contingencies/v1.tex

@@ -140,6 +140,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 threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment—even when core assumptions prove invalid, the research produces valuable contributions.
+This section identifies barriers to success by answering the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment—even when core assumptions prove invalid, the research produces valuable contributions that advance the field.
 
-The technical research plan is now complete. What will be done (Section 3), how success will be measured (Section 4), and what might prevent it (this section) have been established. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers these questions by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.
+The technical research plan is now complete. What will be done (Section 3), how success will be measured (Section 4), and what might prevent it (this section) have been established. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector.

6-broader-impacts/v1.tex

@@ -10,9 +10,9 @@ 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. 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 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.
+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: 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 approximately 23--30\% of total levelized cost, translating to \$21--28 billion annually for projected datacenter demand.
 
-\textbf{What difference will 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.
+\textbf{What difference will it make?} This research directly addresses the \$21--28 billion annual O\&M cost challenge. High-assurance autonomous control makes small modular reactors economically viable for datacenter power while maintaining nuclear safety standards.
 
 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, which 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
 specifications automates routine operational sequences that currently require