Editorial pass: tactical and operational improvements

- Improved sentence-level clarity using Gopen's principles (issue-point, topic-stress)
- Combined choppy sentences for better flow
- Strengthened verbs and reduced passive voice
- Improved paragraph transitions and section coherence
- Maintained technical precision while enhancing readability

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

@@ -30,9 +30,9 @@ Safety systems already employ extensive automation. Reactor Protection Systems t
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge: even 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. Training alone cannot eliminate these failures.
+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.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These

3-research-approach/v3.tex

@@ -152,7 +152,7 @@ Tactical control manages individual components—pumps, turbines, and chemistry.
 
 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.
+Consider refueling as an example. The strategic level sets the refueling schedule. The tactical level maintains core temperature. The operational level issues the shutdown procedure, achieving the strategic goal through several smaller tactical objectives.
 
 This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution determining which tactical control law applies. Together, these two levels form the complete hybrid system. This operational level becomes the target for autonomous control because it bridges strategic intent with tactical execution through discrete mode-switching decisions.
 
@@ -262,9 +262,7 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh
 
 The previous subsection demonstrated how 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?
 
-Reactive synthesis bridges this gap by automatically constructing 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. The current discrete state and status of guard conditions form the input; the next discrete state forms the output.
+Reactive synthesis bridges this gap by automatically constructing controllers guaranteed to satisfy temporal logic specifications. It automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. The current discrete state and guard condition status form the input; the next discrete state forms the output.
 
 Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ specifying desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller exists. Unrealizable specifications indicate conflicting or impossible requirements in
 the original procedures—this realizability check catches errors before implementation. 
@@ -291,11 +289,11 @@ Reactive synthesis produces discrete mode-switching logic from procedures. The n
 
 \subsection{Continuous Control Modes}
 
-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.
+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.
 
 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. 
 
-This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification: model checking confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that capability exists. The contribution lies in the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, which confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that capability exists. The contribution lies in the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
 The operational control scope defines go/no-go decisions that determine what
 kind of continuous control to implement. The entry or exit conditions of a
@@ -394,9 +392,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Reachability analysis verifies whether the target can be reached.
+Transitory modes drive the system toward exit conditions, with reachability analysis verifying whether the target can be reached.
 
-Stabilizing modes address a different question: will the system stay within bounds? These 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.
+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.
 
 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
@@ -445,7 +443,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types handle nominal operations. Transitory modes move the plant between conditions using reachability analysis. Stabilizing modes maintain the plant within regions using barrier certificates. Both assume the plant dynamics match the design model.
+Transitory and stabilizing modes handle nominal operations—moving the plant between conditions and maintaining it within regions, respectively—but 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.
 

4-metrics-of-success/v1.tex

@@ -2,9 +2,9 @@
 
 \textbf{Heilmeier Question: How will success be measured?}
 
-Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. The approach 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? 
+Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control and 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). At TRL 5, 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 measure success appropriately, 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. 
 

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—a definition that assumes critical technical challenges can be overcome.
 
-Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5. First, computational tractability of synthesis and verification. Second, complexity of the discrete-continuous interface. Third, completeness of procedure formalization.
+Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 
 Each risk has identifiable early warning indicators and viable mitigation strategies. 
 
@@ -12,7 +12,7 @@ Each risk carries associated early warning indicators and contingency plans that
 
 \subsection{Computational Tractability of Synthesis}
 
-Computational tractability represents the first major risk. The core 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 from complete startup procedures may produce automata with thousands of states. Synthesis times may exceed days or weeks. This would prevent completion within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove intractable. Either barrier would constitute a fundamental obstacle.
+Computational tractability represents the first major risk. The core assumption—that formalized startup procedures will yield automata small enough for efficient synthesis and verification—may fail. Reactive synthesis scales exponentially with specification complexity; temporal logic specifications from complete startup procedures may produce automata with thousands of states requiring synthesis times of days or weeks, preventing completion within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove intractable. Either barrier would constitute a fundamental obstacle.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets

6-broader-impacts/v1.tex

@@ -2,9 +2,9 @@
 
 \textbf{Heilmeier Questions: Who cares? Why now? What difference will it make?}
 
-Sections 2 through 5 established the complete technical research plan. Section 2 addressed what has been done. Section 3 explained what is new and why it will succeed. Section 4 defined how to measure success. Section 5 identified what could prevent success.
+Sections 2 through 5 established the complete technical research plan: what has been done, what is new and why it will succeed, how to measure success, and what could prevent success.
 
-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.
+This section addresses the remaining Heilmeier questions by connecting 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 competitive with fossil alternatives. All three stakeholders require autonomous control with safety guarantees.
 
@@ -12,7 +12,7 @@ The technical plan is complete. This section addresses the remaining Heilmeier q
 
 \textbf{Why now?} Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis, creating a market demanding 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. At this scale, nuclear power economics demand careful attention to operating costs.
+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) for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions, but at this scale, nuclear power economics demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook 2022 projects advanced nuclear power entering service in 2027 will cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is projected to reach 1,050 terawatt-hours annually by 2030~\cite{eesi_datacenter_2024}. Nuclear power supplying this demand would generate total annual costs exceeding \$92 billion. 
 

8-schedule/v1.tex

@@ -4,7 +4,7 @@
 
 Section 6 demonstrated that this work addresses a \$21--28 billion annual cost barrier and establishes a generalizable framework for safety-critical autonomous systems. This final section addresses the last Heilmeier question: How long will it take?
 
-This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources. The work progresses sequentially through three main research thrusts, culminating in integrated demonstration and validation.
+This research will be conducted over six trimesters (24 months) of full-time effort following the proposal defense in Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC Fellowship provide all computational and experimental resources, with work progressing sequentially through three main research thrusts and culminating in integrated demonstration and validation.
 
 The first semester (Spring 2026) focuses on Thrust 1, translating startup
 procedures into formal temporal logic specifications using FRET. This

main.aux

@@ -1,57 +1,58 @@
 \relax 
-\providecommand \oddpage@label [2]{}
 \@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
 \citation{NUREG-0899,10CFR50.34}
 \citation{10CFR55.59}
 \citation{WRPS.Description,gentillon_westinghouse_1999}
+\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
 \citation{operator_statistics}
 \citation{10CFR55}
 \citation{10CFR50.54}
-\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
 \citation{Kemeny1979}
 \citation{WNA2020}
 \citation{hogberg_root_2013}
 \citation{zhang_analysis_2025}
-\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
 \citation{Kiniry2024}
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent }
+\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS: The State of Formal Methods in Nuclear Control}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Differential Dynamic Logic: Post-Hoc Hybrid Verification}{6}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Summary: The Verification Gap}{6}{}\protected@file@percent }
 \citation{HANDBOOK ON HYBRID SYSTEMS}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
-\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
-\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
-\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
-\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{10}{}\protected@file@percent }
+\newlabel{fig:hybrid_automaton}{{1}{10}{Research Approach}{figure.1}{}}
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{11}{}\protected@file@percent }
+\newlabel{fig:strat_op_tact}{{2}{11}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{12}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Continuous Control Modes}{13}{}\protected@file@percent }
 \citation{MANYUS THESIS}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{14}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{16}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{17}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{19}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{19}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{19}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{22}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{22}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{22}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{24}{}\protected@file@percent }
 \citation{eia_lcoe_2022}
 \citation{eesi_datacenter_2024}
 \citation{eia_lcoe_2022}
-\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{26}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{29}{}\protected@file@percent }
+\gtt@chartextrasize{0}{164.1287pt}
+\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{29}{}\protected@file@percent }
+\newlabel{fig:gantt}{{3}{29}{Schedule, Milestones, and Deliverables}{figure.3}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{29}{}\protected@file@percent }
 \bibstyle{ieeetr}
 \bibdata{references}
-\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent }
-\gtt@chartextrasize{0}{164.1287pt}
-\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent }
-\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent }
 \bibcite{NUREG-0899}{1}
 \bibcite{10CFR50.34}{2}
 \bibcite{10CFR55.59}{3}
@@ -64,8 +65,8 @@
 \bibcite{WNA2020}{10}
 \bibcite{hogberg_root_2013}{11}
 \bibcite{zhang_analysis_2025}{12}
+\@writefile{toc}{\contentsline {section}{References}{30}{}\protected@file@percent }
 \bibcite{Kiniry2024}{13}
 \bibcite{eia_lcoe_2022}{14}
 \bibcite{eesi_datacenter_2024}{15}
-\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent }
-\gdef \@abspage@last{27}
+\gdef \@abspage@last{34}

main.toc

@@ -2,26 +2,28 @@
 \contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
 \contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}%
 \contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}%
-\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}%
+\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}%
 \contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}%
-\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
-\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}%
-\contentsline {section}{\numberline {3}Research Approach}{7}{}%
-\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
-\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
-\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
-\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}%
-\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}%
-\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}%
-\contentsline {section}{\numberline {4}Metrics for Success}{15}{}%
-\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}%
-\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}%
-\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}%
-\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}%
-\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}%
-\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}%
-\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}%
-\contentsline {section}{\numberline {6}Broader Impacts}{20}{}%
-\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}%
-\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}%
-\contentsline {section}{References}{23}{}%
+\contentsline {subsubsection}{\numberline {2.3.1}HARDENS: The State of Formal Methods in Nuclear Control}{5}{}%
+\contentsline {subsubsection}{\numberline {2.3.2}Differential Dynamic Logic: Post-Hoc Hybrid Verification}{6}{}%
+\contentsline {subsection}{\numberline {2.4}Summary: The Verification Gap}{6}{}%
+\contentsline {section}{\numberline {3}Research Approach}{8}{}%
+\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}%
+\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{12}{}%
+\contentsline {subsection}{\numberline {3.3}Continuous Control Modes}{13}{}%
+\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{14}{}%
+\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{15}{}%
+\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{16}{}%
+\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{17}{}%
+\contentsline {section}{\numberline {4}Metrics for Success}{19}{}%
+\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{19}{}%
+\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{19}{}%
+\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{20}{}%
+\contentsline {section}{\numberline {5}Risks and Contingencies}{22}{}%
+\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{22}{}%
+\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{22}{}%
+\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{24}{}%
+\contentsline {section}{\numberline {6}Broader Impacts}{26}{}%
+\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{29}{}%
+\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{29}{}%
+\contentsline {section}{References}{30}{}%