Editorial pass: tactical, operational, and strategic improvements

TACTICAL (sentence-level):
- Improved topic-stress positioning throughout
- Strengthened verb choices (prefer active voice)
- Reduced wordiness while maintaining precision
- Fixed parallel structure in lists

OPERATIONAL (paragraph-level):
- Enhanced transitions between subsections
- Improved paragraph flow and coherence
- Consolidated related ideas for clarity

STRATEGIC (document-level):
- Sharpened Heilmeier question answers
- Improved cross-section linkage
- Ensured consistent framing throughout

All changes preserve technical content and argument structure while
improving clarity and impact.

1-goals-and-outcomes/research_statement_v1.tex

@@ -7,13 +7,13 @@ Nuclear reactors today require human operators to follow detailed written proced
 Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if safety assurance equals or exceeds that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods from computer science with control theory to produce hybrid control systems correct by construction.
+This research unifies formal methods from computer science with control theory to produce 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic 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, structuring requirements by scope, condition, component, timing, and response. Realizability checking then 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—satisfy each discrete mode's requirements.
 
-Continuous modes classify by control objective 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. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Continuous modes classify by control objective 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. The methodology will demonstrate 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

@@ -15,7 +15,7 @@ This research unifies formal methods with control theory to produce hybrid contr
 % 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 verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % 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 transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers that are provably free from design defects. 
+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. Together, these steps transform operating procedures into logical specifications that constrain continuous dynamics, producing 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.
 
@@ -27,14 +27,14 @@ If successful, this approach produces three concrete outcomes:
   % OUTCOME 1 Title
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
-    A methodology converts written operating procedures into formal
+    The methodology converts written operating procedures into formal
     specifications. Reactive synthesis tools then automatically generate
     discrete control logic from these specifications. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
     % Outcome
-    Control system engineers can generate verified mode-switching controllers
-    directly from regulatory procedures. They need no formal methods expertise.
-    This lowers the barrier to high-assurance control systems.
+    Control engineers can generate verified mode-switching controllers
+    directly from regulatory procedures without formal methods expertise,
+    lowering the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}

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

@@ -14,7 +14,7 @@ Current practice rests on two critical components: procedures and operators. Pro
 
 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, while 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 rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available time, or that transitions between procedure sets maintain safety invariants.
+Procedure development rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms procedures cover all possible plant states, required actions complete within available time, or 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
@@ -32,7 +32,7 @@ Safety systems already employ extensive automation. Reactor Protection Systems t
 
 Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when executed 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 cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do, while operators determine when and how to act. This discretion introduces persistent failure modes training cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -89,7 +89,7 @@ implementations directly from Cryptol models---eliminating the traditional gap
 between specification and implementation where errors commonly arise.
 
 Despite its accomplishments, HARDENS has a fundamental limitation for hybrid control synthesis: the project addressed only discrete digital control logic. Continuous reactor dynamics remained unmodeled and unverified.
-The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation. The closed-loop hybrid system behavior remained unverified.
+The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation, leaving the closed-loop hybrid system behavior unverified.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -159,11 +159,11 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 This section addressed two Heilmeier questions: What has been done? What are the limits of current practice?
 
-\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. First, human operators provide operational flexibility but introduce persistent reliability constraints that training cannot eliminate. Second, HARDENS verified discrete logic but omitted continuous dynamics. Third, differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
+\textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. First, human operators provide operational flexibility but introduce persistent reliability constraints training cannot eliminate. Second, HARDENS verified discrete logic but omitted continuous dynamics. Third, 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?} 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—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 and technical maturity. Small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants, while formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
+\textbf{Why now?} Two forces create urgency: economic necessity and technical maturity. Small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants, while formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
 This section established what has been done and the limits of current practice. The verification gap is clear: no existing methodology synthesizes provably correct hybrid controllers from operational procedures. The timing is right: economic pressures demand autonomous control while technical maturity enables it. 
 

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 either discrete switching logic or continuous control behavior—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, and both consume enormous resources.
+Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees, and both consume enormous resources.
 
 This approach bridges that 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: 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, creating discontinuities traditional verification techniques cannot handle directly.
 
-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; 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,14 +58,14 @@ 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 either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently and have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology. Prior work cannot span from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
 \begin{enumerate}
-\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems.
-\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—allowing appropriate verification tools to match each mode type and enabling mode-local analysis with provable composition guarantees.
-\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, providing existing structure that avoids artificial abstractions and makes the approach tractable for complex systems like nuclear reactor startup.
+\item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, discrete synthesis defines entry/exit/safety contracts bounding continuous verification, transforming an intractable global problem into tractable local problems.
+\item \textbf{Mode classification:} Continuous modes classify by control objective—transitory, stabilizing, or expulsory—matching appropriate verification tools to each mode type and enabling mode-local analysis with provable composition guarantees.
+\item \textbf{Procedure-driven structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, providing existing structure avoiding artificial abstractions and making the approach tractable for complex systems like nuclear reactor startup.
 \end{enumerate}
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed.
@@ -144,7 +144,7 @@ These factors combine to demonstrate feasibility on production control systems w
 
 The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. This formalism provides the mathematical structure for hybrid control. But a critical question remains: where do these formal descriptions originate?
 
-The answer lies in existing practice. Nuclear operations already possess a natural hybrid structure that maps directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures rather than imposing artificial abstractions.
+The answer lies in existing practice. Nuclear operations already possess a natural hybrid structure mapping directly to this formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge, leveraging decades of domain expertise already encoded in operating procedures rather than imposing artificial abstractions.
 
 Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years: managing labor needs and supply chains to optimize scheduled maintenance and downtime.
 
@@ -190,7 +190,7 @@ This structure reveals why the operational and tactical levels fundamentally for
 \end{figure}
 
 
-This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by following prescriptive operating manuals where strict procedures govern what control to implement at any given time.
+This operational control level explains why nuclear control requires human operators: the hybrid nature of this control system makes proving controller performance against strategic requirements difficult, and no unified infrastructure exists for building and verifying hybrid systems. Humans fill this layer because their general intelligence provides a safe way to manage the system's hybrid nature by following prescriptive operating manuals, where strict procedures govern what control to implement at any given time.
 
 These procedures provide the key to HAHACS construction, which leverages two observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe implementation rules before construction begins, meaning a HAHACS's intended behavior can be completely specified before implementation. Requirements define the behavior of any control system: statements about what
 the system must do, must not do, and under what conditions. For nuclear systems,
@@ -392,9 +392,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions, and reachability analysis verifies whether the target can be reached.
+Transitory modes drive the system toward exit conditions, and reachability analysis verifies whether the target can be reached. Stabilizing modes address a different question.
 
-Stabilizing modes address a different question: will the system stay within bounds? Unlike transitory modes that aim to reach a target, 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.
+Rather than asking "can the system reach a target?" stabilizing modes ask "will the system stay within bounds?" Unlike transitory modes that aim to reach a target, 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?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -443,7 +443,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations. Transitory modes move the plant between conditions. Stabilizing modes maintain it within regions. Both assume the plant dynamics match the design model.
+Transitory and stabilizing modes handle nominal operations—transitory modes move the plant between conditions while stabilizing modes maintain it within regions. Both assume the plant dynamics match the design model.
 
 Expulsory modes address a different scenario: situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
 
@@ -528,7 +528,7 @@ This section addressed two critical Heilmeier questions: What is new? Why will i
 
 \textbf{What is new?} Three innovations enable compositional verification by integrating reactive synthesis, reachability analysis, and barrier certificates: 
 
-First, \textit{contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
+First, \textit{contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts bounding continuous verification. 
 
 Second, \textit{mode classification} enables mode-local analysis with provable composition guarantees by matching continuous modes to appropriate verification tools. 
 
@@ -538,19 +538,19 @@ Section 2 established that prior work verified discrete logic or continuous dyna
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility: 
 
-\textit{Existing structure.} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without artificial abstractions. 
+\textit{Existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without artificial abstractions. 
 
-\textit{Bounded complexity.} Mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
+\textit{Bounded complexity:} Mode-level verification bounds each verification problem locally, avoiding the state explosion making global hybrid system analysis intractable. 
 
-\textit{Industrial validation.} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
+\textit{Industrial validation:} Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
 
 The complete technical methodology is now established. 
 
 Sections 2 and 3 addressed the first four Heilmeier questions. Section 2 established what has been done and what limits current practice. Section 3 explained what is new and why it will succeed. 
 
-Three questions remain. How will success be measured? What could prevent success? Who cares, why now, and what difference will this work make? 
+Three questions remain: How will success be measured? What could prevent success? Who cares, why now, and what difference will this work make? 
 
-Section 4 addresses the first question: metrics for success. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
+Section 4 addresses metrics for success. Section 5 identifies what could prevent success. Section 6 explains who cares, why now, and what difference this work will make.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -4,11 +4,11 @@
 
 Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. It will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. This section addresses the next Heilmeier question: How will success be measured? 
 
-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.
+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 appropriately measure success, then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric for work bridging academic proof-of-concept and practical deployment. 
 
-Academic metrics—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—simulation accuracy or computational speed—fail to demonstrate theoretical rigor. TRLs measure both.
+Academic metrics—papers published or theorems proved—fail to capture practical feasibility. Empirical metrics—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. The system moves from individual components to integrated hardware testing. Two requirements constrain this progression. First: formal verification must remain valid throughout. Second: the proofs must compose as the system scales.
 

5-risks-and-contingencies/v1.tex

@@ -137,7 +137,7 @@ This section answered the Heilmeier question: What could prevent success?
 
 Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each has viable mitigation strategies preserving research value even when core assumptions fail.
 
-The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. This design maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain.
+The staged project structure ensures partial success yields publishable results identifying remaining deployment barriers. This design maintains contribution regardless of which technical obstacles prove insurmountable. Even failure advances the field by documenting precisely which barriers remain.
 
 Sections 2 through 5 established the complete technical research plan. 
 

6-broader-impacts/v1.tex

@@ -22,7 +22,7 @@ Operations and maintenance represents a substantial component. The EIA estimates
 
 Current nuclear operations require full control room staffing for each reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output. This makes per-megawatt costs prohibitive. These staffing requirements drive the economic challenge threatening SMR deployment for datacenter applications.
 
-Synthesizing provably correct hybrid controllers from formal specifications automates routine operational sequences that currently require constant human oversight. This enables a fundamental shift from direct operator control to supervisory monitoring. Operators oversee multiple autonomous reactors rather than manually controlling individual units.
+Synthesizing provably correct hybrid controllers from formal specifications automates routine operational sequences currently requiring constant human oversight. This enables a fundamental shift from direct operator control to supervisory monitoring, where operators oversee multiple autonomous reactors rather than manually controlling individual units.
 
 The correct-by-construction methodology proves critical for this transition.
 Traditional automation approaches cannot provide sufficient safety guarantees
@@ -64,9 +64,9 @@ adoption across critical infrastructure.
 
 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{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 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{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 and 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.