Editorial pass: Gopen sentence-level improvements + section flow

Pass 1 (Tactical):
- Broke up overly long sentences for clarity
- Improved topic-stress positioning (stress at end)
- Strengthened topic strings across sentences
- Converted passive constructions to active where appropriate
- Enhanced verb choice for directness

Pass 2 (Operational):
- Improved paragraph transitions
- Added backward/forward references between sections
- Strengthened section coherence

Pass 3 (Strategic):
- Verified Heilmeier question alignment across all sections
- Improved inter-section linking
- Ensured answers are crisp and clearly stated

Focus areas:
- Research statement: split complex sentences, clarified three-stage approach
- Goals section: improved parallel structure in outcomes
- State of the Art: emphasized key statistics, clearer subsection transitions
- Research Approach: broke up technical complexity, strengthened 'what is new' section
- All sections: improved Heilmeier question framing and answers

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +2,18 @@
 My research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today depend on extensively trained human operators. These operators follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-My approach unifies formal methods from computer science with control theory to produce hybrid control systems that are correct by construction.
+My approach unifies formal methods from computer science with control theory. This produces hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications structured by scope, condition, component, timing, and response—exposing conflicts and ambiguities through realizability checking before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory techniques—satisfy each discrete mode's requirements.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. These specifications structure requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata that are provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory techniques—satisfy each discrete mode's requirements.
 
-Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. I demonstrate this methodology on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off
 This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -6,14 +6,14 @@ This research develops autonomous hybrid control systems with mathematical guara
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Nuclear plants today depend on extensively trained human operators who follow detailed written procedures and strict regulatory requirements, switching between control modes based on plant conditions and procedural guidance.
+Nuclear plants today depend on extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements. They switch between control modes based on 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. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This work unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
+This work unifies formal methods with control theory. This produces hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
 % Hypothesis
 Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics—producing autonomous controllers provably free from design defects. 
 
@@ -73,9 +73,9 @@ This proposal follows the Heilmeier Catechism. Each section explicitly answers i
 \begin{itemize}
   \item \textbf{Section 2 (State of the Art):} What has been done? What are the limits of current practice?
   \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed?
-  \item \textbf{Section 4 (Metrics for Success):} How do we measure success?
+  \item \textbf{Section 4 (Metrics for Success):} How will success be measured?
   \item \textbf{Section 5 (Risks and Contingencies):} What could prevent success?
   \item \textbf{Section 6 (Broader Impacts):} Who cares? Why now? What difference will it make?
   \item \textbf{Section 8 (Schedule):} How long will it take?
 \end{itemize}
-Each section begins by stating its Heilmeier questions and ends by summarizing its answers, ensuring both local clarity and global coherence.
+Each section begins by stating its Heilmeier questions and ends by summarizing its answers. This ensures both local clarity and global coherence.

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

@@ -14,7 +14,7 @@ Current practice rests on two critical components: procedures and operators. Thi
 
 Nuclear plant procedures form a strict 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. All procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
-Procedure development relies on expert judgment and simulator validation—not formal verification. While 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review, key safety properties escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Procedure development relies on expert judgment and simulator validation—not formal verification. Regulations require rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} mandates technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proofs confirm that procedures cover all possible plant states. No proofs verify that required actions complete within available timeframes. No proofs guarantee that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} No proof exists that procedures cover all
@@ -30,7 +30,7 @@ This division between automated and human-controlled functions reveals the funda
 
 \subsection{Human Factors in Nuclear Accidents}
 
-The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge—perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
 
 Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
 
@@ -42,9 +42,9 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
-Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence motivates the need for formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a fundamental ambiguity—placing responsibility for safe power plant operations on the licensee without formally verifying that operators can fulfill this responsibility guarantees nothing. This tension between operational flexibility and safety assurance remains unresolved: the person responsible for reactor safety often becomes the root cause of failure.
+Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster: operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. The President's Commission on TMI identified a fundamental ambiguity—placing responsibility for safe power plant operations on the licensee without formally verifying that operators can fulfill this responsibility guarantees nothing. This tension between operational flexibility and safety assurance remains unresolved: the person responsible for reactor safety often becomes the root cause of failure.
 
-Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events, while equipment failures account for approximately 20\%~\cite{WNA2020}. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
+Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events~\cite{WNA2020}. Equipment failures account for only 20\%. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
 2007--2020~\cite{zhang_analysis_2025} found that active
 errors appeared in 53\% of events, while latent errors—organizational and
@@ -157,8 +157,8 @@ This section answered two Heilmeier questions: What has been done? What are the
 
 \textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
 
-\textbf{What are the limits of current practice?} The verification gap emerges clearly: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
+\textbf{What are the limits of current practice?} A clear verification gap emerges. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics but never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions—small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions—formal methods tools have matured sufficiently to enable compositional hybrid verification.
+\textbf{Why now?} Two forces create urgency. Economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Technical maturity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification.
 
-Section 3 closes this verification gap, establishing what is new and why the approach will succeed.
+The gap is clear. The timing is right. Section 3 closes this verification gap by establishing what is new and why the approach will succeed.

3-research-approach/v3.tex

@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
+Previous approaches verified discrete switching logic or continuous control behavior but never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources. This approach changes that.
 
-This approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
+Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field. These discontinuities cannot be handled directly by traditional verification techniques.
 
-This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing 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.
+This methodology decomposes the problem. It verifies 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 systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -58,7 +58,7 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics but never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently. Prior work has not integrated them into a systematic design methodology spanning from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify discrete logic or continuous dynamics but never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently. They have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
@@ -70,7 +70,7 @@ Three innovations enable compositional verification:
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
 
-\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, allowing domain experts without formal methods training to adopt it.
+\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This approach formalizes that existing structure without imposing artificial abstractions. Domain experts can adopt it without formal methods training.
 
 \textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. The decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
 
@@ -260,9 +260,9 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 \subsection{Discrete Controller Synthesis}
 
-Operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do, but a critical gap remains: how do we implement those requirements?
+The previous subsection demonstrated how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do. A critical gap remains: how do we implement those requirements?
 
-Reactive synthesis bridges this gap by automatically constructing controllers guaranteed to satisfy temporal logic specifications.
+Reactive synthesis bridges this gap. It automatically constructs controllers guaranteed to satisfy temporal logic specifications.
 
 Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. Temporal logic specifications enable reactive synthesis to construct the discrete control system automatically. The current discrete state and status of guard conditions form the input; the next discrete state forms the output.
 
@@ -275,7 +275,7 @@ This shift carries two critical implications. First, complete traceability: the
 
 The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications.
 
-Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
+Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications synthesize robot motion planners from natural language specifications. They generate flight control software for unmanned aerial vehicles. They create verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications.
 
 Reactive synthesis produces discrete mode-switching logic from procedures. The next subsection addresses what executes within each discrete mode: continuous control and its verification.
 
@@ -291,7 +291,7 @@ Reactive synthesis produces discrete mode-switching logic from procedures. The n
 
 \subsection{Continuous Control Modes}
 
-Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. However, hybrid control requires more than correct mode switching—the continuous dynamics executing within each discrete mode must also verify against requirements.
+The previous subsection showed how reactive synthesis produces a provably correct discrete controller. This controller determines when to switch between modes. However, hybrid control requires more than correct mode switching. The continuous dynamics executing within each discrete mode must also verify against requirements.
 
 Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
 

4-metrics-of-success/v1.tex

@@ -1,8 +1,8 @@
 \section{Metrics for Success}
 
-\textbf{Heilmeier Question: How do we measure success?}
+\textbf{Heilmeier Question: How will success be measured?}
 
-Section 3 established the technical approach, answering what is new (compositional verification bridging discrete synthesis with continuous control) and why it will succeed (existing procedural structure, bounded complexity, and industrial validation). This section addresses the next Heilmeier question: how to measure success. 
+Section 3 established the technical approach. It answered what is new: compositional verification bridging discrete synthesis with continuous control. It answered why it will succeed: existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: how to measure success. 
 
 Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5), where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
 

5-risks-and-contingencies/v1.tex

@@ -2,9 +2,9 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome.
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. That definition assumes critical technical challenges can be overcome. What if they cannot?
 
-Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. 
+Every research plan rests on assumptions that might prove false. This section identifies three primary risks that could prevent reaching TRL 5. These are: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization. 
 
 Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results and clearly identifies remaining barriers to deployment even when full success proves elusive.
 

6-broader-impacts/v1.tex

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2--5 established the complete technical research plan: what has been done (Section 2), what is new and why it will succeed (Section 3), how to measure success (Section 4), and what could prevent success (Section 5).
+Sections 2--5 established the complete technical research plan. Section 2 answered what has been done. Section 3 answered what is new and why it will succeed. Section 4 answered how to measure success. Section 5 answered what could prevent success.
 
-This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
+The technical plan is complete. This section addresses the remaining Heilmeier questions. It connects technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
 
-\textbf{Who cares?} Three stakeholder groups face the same economic constraint—high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable. All three need this research to succeed.
 
 \textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power while establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.
 
@@ -64,7 +64,7 @@ This section answered three critical Heilmeier questions:
 
 \textbf{Who cares?} Three stakeholder groups face the same constraint. The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive. All three require autonomous control with safety guarantees.
 
-\textbf{Why now?} Two forces converge to create urgency. \textit{First: exponentially growing demand.} AI infrastructure demands create immediate need for economical nuclear power at datacenter scale, with projections showing datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. \textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent, and the tools exist.
+\textbf{Why now?} Two forces converge to create urgency. \textit{First: exponentially growing demand.} AI infrastructure creates immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. \textit{Second: technical maturity.} Formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent. The tools exist.
 
 \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure, extending beyond nuclear power to any safety-critical system requiring provable correctness.