Copy edit: Tactical improvements (Gopen principles)

- Active voice throughout (I/my instead of 'this research')
- Shorter sentences for clarity and impact
- Stronger topic-stress positioning
- Improved topic strings and paragraph flow
- More direct, punchy language in key arguments
- Better readability without changing technical content

1-goals-and-outcomes/research_statement_v1.tex

@@ -1,5 +1,5 @@
 % GOAL PARAGRAPH
-This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
+I develop autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Today's nuclear reactors depend on human operators with extensive training. These operators follow detailed written procedures and switch between control objectives based on plant conditions.
@@ -7,13 +7,13 @@ Today's nuclear reactors depend on human operators with extensive training. Thes
 Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant supervision—but only with assurance equal to or exceeding human-operated systems.
 
 % APPROACH PARAGRAPH Solution
-This research produces hybrid control systems correct by construction, combining formal methods from computer science with control theory. 
+I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. 
 % Rationale
 Human operators already work this way: discrete logic switches between continuous control modes. Formal methods alone fail because they generate provably correct switching logic but cannot handle the continuous dynamics governing transitions. Control theory alone also fails because it verifies continuous behavior but cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
 % 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 exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Standard control theory techniques design these continuous controllers.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. FRET structures requirements by scope, condition, component, timing, and response—realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques.
 
-Control objectives classify continuous modes into three types: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove safe mode transitions, enabling local verification without global trajectory analysis. An Emerson Ovation control system will demonstrate the methodology.
+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 safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates 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, directly addressing the economic constraints threatening small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -1,7 +1,7 @@
 \section{Goals and Outcomes}
 
 % GOAL PARAGRAPH
-This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
+I develop autonomous hybrid control systems with mathematical guarantees of safe and correct behavior.
 
 % 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.
@@ -11,11 +11,11 @@ Today's nuclear plants depend on human operators with extensive training. These
 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 their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only with assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-This research produces hybrid control systems correct by construction, combining formal methods with control theory.
+I produce hybrid control systems correct by construction, unifying formal methods with control theory.
 % 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 fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
+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 continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together.
 % Hypothesis
-Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. Operating procedures formalize into logical specifications that constrain continuous dynamics, producing autonomous controllers provably free from design defects. 
+Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This approach formalizes 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.
 
@@ -64,7 +64,7 @@ If successful, this approach produces three concrete outcomes:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification to close that gap. The key innovation treats discrete specifications as contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 examines why prior work has not achieved this integration. Section 3 details how this integration will be accomplished.
+\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification to close that gap. The key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 examines why prior work fails at this integration. Section 3 details how I accomplish it.
 
 % Outcome Impact
 If successful, control engineers create autonomous controllers from

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

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-This section answers these questions by examining how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis: reactor operators and their operating procedures, the fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
+This section answers these questions by examining how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis. First, reactor operators and their operating procedures. Second, fundamental limitations of human-based operation. Third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis.
 
 \subsection{Current Reactor Procedures and Operation}
 
@@ -81,10 +81,8 @@ synthesis generated verifiable C implementations and SystemVerilog hardware
 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, leaving continuous reactor dynamics unmodeled and unverified.
+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
+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 the interaction 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 went unverified.
-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 the interaction between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation, not the closed-loop hybrid system behavior.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control
@@ -117,7 +115,7 @@ primary assurance evidence.
 
 \subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction by extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). 
+HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified. Other researchers attacked the problem from the opposite direction. They extended temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). 
 
 While dL addresses continuous dynamics, it encounters different limitations. dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
@@ -164,6 +162,6 @@ No existing approach addresses both discrete and continuous verification composi
 
 \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. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-Two imperatives converge to make closing this gap urgent: economic necessity (small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants) and technical opportunity (formal methods tools have matured sufficiently to enable compositional hybrid verification). 
+Two imperatives converge to make closing this gap urgent. Economic necessity: small modular reactors cannot compete economically with per-megawatt staffing costs matching large conventional plants. Technical opportunity: formal methods tools have matured sufficiently to enable compositional hybrid verification. 
 
-Section 3 addresses this verification gap by establishing what makes the proposed approach new and why it will succeed.
+Section 3 addresses this verification gap. It establishes what makes my approach new and why it will succeed.

3-research-approach/v3.tex

@@ -19,9 +19,9 @@ This section answers these questions by presenting the complete technical approa
 % ----------------------------------------------------------------------------
 % 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 and 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 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. Both consume enormous resources.
 
-This work bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata.
+I bridge that gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly.
 
@@ -52,7 +52,9 @@ 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 each exist independently. Prior work has not integrated them into a systematic design methodology spanning procedures to verified implementation. Three innovations enable this integration:
+\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 each exist independently. Prior work has not integrated them into a systematic design methodology spanning procedures to verified implementation. 
+
+Three innovations enable this integration:
 
 \begin{enumerate}
 \item \textbf{Contract-based decomposition:} This approach inverts the traditional structure. 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.
@@ -62,11 +64,11 @@ A HAHACS requires this tuple together with proof artifacts demonstrating that th
 
 \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. This work formalizes existing structure. It does not impose artificial abstractions. Domain experts without formal methods training can adopt the approach.
+\textbf{First, existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. I formalize existing structure—I do not impose artificial abstractions. Domain experts without formal methods training can adopt the approach.
 
-\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts. It avoids attempting global hybrid system analysis. This decomposition bounds computational complexity. It transforms an intractable global problem into tractable local verifications.
+\textbf{Second, bounded complexity:} Mode-level verification checks each mode against local contracts. This avoids attempting global hybrid system analysis. The decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications.
 
-\textbf{Third, industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. Solutions address real deployment constraints, not just theoretical correctness.
+\textbf{Third, industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. My solutions address real deployment constraints, not just theoretical correctness.
 
 These factors combine to demonstrate 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.
 
@@ -142,9 +144,9 @@ The approach does not impose artificial abstractions. Instead, it constructs for
 
 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.
 
-The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems—continuous systems that directly impact the physical state of the plant by maintaining pressurizer level, core temperature, and reactivity through chemical shim.
+The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems—continuous systems that maintain pressurizer level, core temperature, and reactivity through chemical shim. These systems directly impact the physical state of the plant.
 
-The operational scope links these extremes and represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
+The operational scope links these extremes. It represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. 
 
 An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective.
 
@@ -230,7 +232,7 @@ eventually reaches operating temperature''), and response properties (``if
 coolant pressure drops, the system initiates shutdown within bounded time'').
 
 
-This work uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. 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: the current nuclear workforce can adopt these tools without extensive formal methods training.
+I use FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.
 
 FRET's key feature is its ability to start with logically imprecise
 statements and refine them consecutively into well-posed specifications. We

4-metrics-of-success/v1.tex

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Question: How do we measure success?}
 
-Section 3 established the technical approach—what will be done and why it will work. This section addresses how we measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
+Section 3 established the technical approach—what I will do and why it will work. This section addresses how I measure whether it actually succeeds. The answer: Technology Readiness Level advancement, progressing from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5).
 
-This work begins at TRL 2--3 and aims to reach TRL 5, where system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric: it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
+My 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. It explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs are the right metric, then defines specific criteria for each level from TRL 3 through TRL 5.
 
-Technology Readiness Levels provide the ideal success metric. They explicitly measure the gap between academic proof-of-concept and practical deployment. This is precisely what this work bridges. 
+Technology Readiness Levels provide the ideal success metric. They explicitly measure the gap between academic proof-of-concept and practical deployment. This is precisely what my 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.
 

5-risks-and-contingencies/v1.tex

@@ -10,7 +10,7 @@ Each risk carries associated early warning indicators. Each has contingency plan
 
 \subsection{Computational Tractability of Synthesis}
 
-Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times exceeding days or weeks and preventing completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
+Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states. Synthesis times may exceed days or weeks, preventing completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -28,7 +28,7 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
 
-This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
 
 The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.
 

6-broader-impacts/v1.tex

@@ -6,13 +6,13 @@ Sections 2--5 established the complete technical research plan: what has been do
 
 This section addresses the remaining Heilmeier questions by connecting technical methodology to economic and societal impact. The answer: this research directly addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems.
 
-The technical approach enables compositional hybrid verification. This capability did not exist before. But why does this matter beyond academic contribution? 
+The technical approach enables compositional hybrid verification—a capability that did not exist before. But why does this matter beyond academic contribution? 
 
 Three stakeholder groups converge on 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.
 
-What has changed? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis—the market now demands solutions that did not exist before.
+What has changed? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis. The market now demands solutions that did not exist before.
 
 Nuclear power presents both a compelling application domain and an urgent economic challenge. Recent interest in powering artificial intelligence infrastructure has renewed focus on small modular reactors (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions. Nuclear power economics at this scale, however, demand careful attention to operating costs.
 
@@ -20,11 +20,9 @@ The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects
 
 \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
+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 that threatens SMR deployment for datacenter applications.
-specifications automates routine operational sequences that currently require
+
-constant human oversight. This enables a fundamental shift from direct operator
+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.
-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