Obsidian/ERLM-Proposal-Review-Detailed.md

# ERLM Proposal Writing Review - Comprehensive Detail

**Date**: December 2, 2025
**Framework**: Gopen's Sense of Structure

---

## How to Use This Document

- **Each issue has a checkbox** `- [ ]` for tracking your revision progress
- **Issues organized by section** and then by level (sentence, paragraph, content)
- **Cross-references to Summary doc** for patterns and principles
- **Work section-by-section** - complete one section before moving to next
- **Check off items as you revise** - provides visual progress tracking

For pattern explanations and principles, see the **Executive Summary** document.

---

## 1. Goals and Outcomes Section

### 1.1 Sentence-Level Issues

- [ ] **Lines 4-6** - Weak stress position
  - Current: "The goal of this research is to develop a methodology for creating autonomous hybrid control systems with mathematical guarantees of safe and correct behavior."
  - Issue: Sentence ends with "correct behavior" (weak, expected). Key innovation is "methodology for creating" with "mathematical guarantees"
  - See Summary: Pattern 1 (Stress Position Weakness)
  - Suggested fix: "The goal of this research is to develop autonomous hybrid control systems that guarantee mathematically safe and correct behavior."

- [ ] **Lines 9-11** - Weak stress position + passive construction
  - Current: "Nuclear power plants require the highest levels of control system reliability, where failures can result in significant economic losses, service interruptions, or radiological release."
  - Issue: List ends with weakest item first (economic losses < radiological release). Also "can result in" is weak
  - Fix: "Nuclear power plants require the highest levels of control system reliability: failures risk radiological release, service interruptions, or significant economic losses."

- [ ] **Lines 13-17** - Buried key claim
  - Current: "Currently, nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to manage reactor control."
  - Issue: Key points (extensively trained, detailed procedures, strict requirements) buried in middle. Ends weakly with "manage reactor control"
  - Fix: "Currently, nuclear plant operations require extensively trained human operators following detailed written procedures under strict regulatory requirements."

- [ ] **Lines 16-17** - Topic position break
  - Current: "These operators make critical decisions about when to switch between different control modes..."
  - Issue: "These operators" okay, but could be tighter as "They" since immediately follows previous sentence about operators
  - Fix: "They make critical decisions..."

- [ ] **Lines 19-20** - Passive "prevents the introduction of"
  - Current: "However, this reliance on human operators prevents the introduction of autonomous control capabilities..."
  - Issue: Nominalization "introduction" + passive "prevents introduction"
  - Fix: "However, this reliance on human operators prevents introducing autonomous control capabilities..." or "...makes autonomous control impossible"

- [ ] **Lines 22-23** - Topic position break
  - Current (new paragraph): "Emerging technologies like small modular reactors face significantly higher..."
  - Issue: Abrupt shift from "reliance on operators" to "emerging technologies"
  - Fix: "This limitation creates particular challenges for emerging technologies like small modular reactors, which face..."

- [ ] **Lines 25-27** - Weak stress position + nominalization
  - Current: "What is needed is a way to create autonomous control systems that can safely manage complex operational sequences..."
  - Issue: Ends with "constant human supervision" (the problem, not the solution). Also "what is needed" is passive framing
  - Fix: "Autonomous control systems must safely manage complex operational sequences with the same assurance as human-operated systems, but without constant human supervision."

- [ ] **Lines 30-31** - Weak stress position
  - Current: "To address this need, we will combine formal methods from computer science with control theory to build hybrid control systems that are correct by construction."
  - Issue: Ends with "correct by construction" which is good, but could emphasize the combination more
  - Fix: "To address this need, we will build hybrid control systems that are correct by construction by combining formal methods from computer science with control theory."

- [ ] **Lines 33-37** - Long complex sentence (45 words)
  - Current: "Hybrid systems use discrete logic to switch between continuous control modes, similar to how operators change control strategies, and existing formal methods can generate provably correct switching logic from written requirements, but they cannot handle the continuous dynamics that occur during transitions between modes."
  - Issue: Two "and" clauses plus a "but" clause—very complex
  - Fix (split): "Hybrid systems use discrete logic to switch between continuous control modes, similar to how operators change control strategies. Existing formal methods can generate provably correct switching logic from written requirements. However, they cannot handle the continuous dynamics that occur during transitions between modes."

- [ ] **Lines 37-39** - Another long complex sentence
  - Current: "Meanwhile, traditional control theory can verify continuous behavior but lacks tools for proving correctness of discrete switching decisions."
  - Issue: This is actually fine as-is, but note the parallel "X can do A but lacks B" structure matches previous sentence well

- [ ] **Lines 40-45** - Very long complex sentence (60+ words)
  - Current: "By synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions, we can create hybrid control systems with end-to-end correctness guarantees. If we can formalize existing procedures into logical specifications and verify that continuous dynamics satisfy transition requirements, then we can build autonomous controllers that are provably free from design defects."
  - Issue: Two long sentences that are somewhat repetitive
  - Fix: Consider combining or cutting redundancy. The first sentence is strong; the second restates it with "if...then" structure that's less confident
  - Suggested: Keep first sentence, delete second, or shorten second to: "This approach yields autonomous controllers provably free from design defects."

- [ ] **Lines 47-48** - Weak stress position
  - Current: "This approach will enable autonomous control in nuclear power plants while maintaining the high safety standards required by the industry."
  - Issue: Ends with "required by the industry"—old information
  - Fix: "This approach will maintain the high safety standards nuclear power plants require while enabling autonomous control."

- [ ] **Lines 50-53** - Long sentence with embedded clause
  - Current: "This work is conducted within the University of Pittsburgh Cyber Energy Center, which provides access to industry collaboration and Emerson control hardware, ensuring that solutions developed are aligned with practical implementation requirements."
  - Issue: "Ensuring that" is weak; also passive "solutions developed"
  - Fix: "This work is conducted within the University of Pittsburgh Cyber Energy Center, which provides industry collaboration and access to Emerson control hardware. This ensures our solutions align with practical implementation requirements."

### 1.2 Paragraph-Level Issues

- [ ] **Lines 3-6 (Goal paragraph)** - Could be stronger
  - Current: Single sentence stating the goal
  - Issue: While clear, could benefit from a second sentence stating why this goal matters (the issue)
  - Fix: Add after line 6: "Such guarantees are essential for safety-critical systems where verification through testing alone cannot provide adequate assurance."

- [ ] **Lines 29-53 (Approach paragraph)** - Too dense, covers multiple sub-topics
  - Current: One large paragraph covering: (1) solution approach, (2) rationale about hybrid systems, (3) existing limitations, (4) hypothesis, (5) payoff, (6) qualifications
  - Issue: This is really 2-3 paragraphs worth of content
  - Fix: Break into two paragraphs:
    - Para 1 (lines 30-38): Solution and rationale
    - Para 2 (lines 40-48): Hypothesis and payoff
    - Keep qualifications (lines 50-53) with payoff or as separate brief paragraph

- [ ] **Outcome paragraphs (58-101)** - Generally strong structure
  - Each outcome has: Title → Strategy → Outcome structure, which is excellent
  - Minor issue: The strategy/outcome distinction could be sharper. Currently reads as "We will do X. Engineers will be able to Y." Consider: "We will do X, enabling engineers to Y."
  - Fix for each:
    - Lines 63-72: Combine last two sentences: "...synthesized into discrete control logic, enabling control system engineers to generate verified mode-switching controllers..."
    - Lines 77-85: Similar combination possible
    - Lines 91-99: Similar combination possible

### 1.3 Content and Organization Issues

- [ ] **Overall structure** - Excellent
  - The four-paragraph opening (goal → problem → approach → outcomes) is very strong
  - The enumerated outcomes are clear and specific
  - Impact paragraph provides good closure
  - No major reorganization needed

- [ ] **Technical detail level** - Appropriate
  - Good balance of specificity (SmAHTR, Emerson hardware) without overwhelming detail
  - Outcomes are concrete and measurable

- [ ] **Missing elements** - None critical
  - All standard goal section elements present
  - Qualifications established
  - Scope clearly defined

---

## 2. State of the Art Section

### 2.1 Sentence-Level Issues

- [ ] **Lines 3-9** - Long opening sentence (46 words)
  - Current: "The principal aim of this research is to create autonomous reactor control systems that are tractably safe. But, to understand what exactly is being automated, it is important to understand how nuclear reactors are operated today."
  - Issue: Two sentences could be more tightly connected
  - Fix: "The principal aim of this research is to create autonomous reactor control systems that are tractably safe. Understanding what we automate requires first understanding current reactor operation."

- [ ] **Lines 6-9** - Roadmap sentence is good but could be punchier
  - Current: "First, the reactor operator themselves is discussed. Then, operating procedures that we aim to leverage later are examined. Next, limitations of human-based operation are investigated, while finally we discuss current formal methods based approaches..."
  - Issue: Passive constructions throughout ("is discussed", "are examined", "are investigated")
  - Fix: "We first discuss the reactor operator, then examine the operating procedures we will leverage, next investigate human operation limitations, and finally review current formal methods approaches to reactor control."

- [ ] **Lines 13-19** - Good opening, solid statistics
  - Current paragraph opener establishes scale and scope well
  - No major issues

- [ ] **Lines 21-34** - Very long paragraph with complex structure
  - Current: "The role of human operators is paradoxically..." through "...fulfill this responsibility under all conditions"
  - Issue: This paragraph tries to do too much: (1) paradox of operator role, (2) TMI example, (3) commission finding
  - Fix: Consider breaking after line 24 (TMI example) into new paragraph

- [ ] **Lines 24-26** - Long embedded quote
  - Current: "operators \"misread confusing and contradictory readings and shut off the emergency water system\""
  - Issue: Long quote breaks sentence flow
  - Fix: Paraphrase or shorten: "operators misread contradictory readings and shut off the emergency water system"

- [ ] **Lines 44-51** - Extremely long sentence (58 words)
  - Current: "These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using guidance from NUREG-0899, but their development process relies fundamentally on expert judgment and simulator validation rather than formal verification. Procedures undergo technical evaluation, simulator validation testing, and biennial review as part of operator requalification under 10 CFR 55.59, but despite these rigorous development processes..."
  - Issue: Actually two long sentences with parallel "X but Y" structure, both 50+ words
  - Fix: Break into shorter sentences: "These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using guidance from NUREG-0899. However, their development process relies on expert judgment and simulator validation rather than formal verification. Procedures undergo technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59. Despite these rigorous processes..."

- [ ] **Lines 48-51** - Weak stress position
  - Current: "...or that transitions between procedure sets maintain safety invariants."
  - Issue: Ends with weakest of three items
  - Fix: Reorder list to build to most important: "...that transitions maintain safety invariants, that actions can be completed within available timeframes, or that procedures cover all possible plant states."

- [ ] **Lines 53-60 (LIMITATION callout)** - Generally strong
  - The bold "LIMITATION:" callouts are excellent framing devices
  - Minor: Some repetition between paragraph text and limitation summary
  - Consider whether limitation box needs all the detail or can be more concise

- [ ] **Lines 74-79** - Topic string break
  - Current: "The current division between automated and human-controlled functions reveals the fundamental challenge..."
  - Previous paragraph ended discussing automatic vs. manual control modes
  - This starts with "current division" which is good topic-position continuity
  - Minor issue: "%%%NEED MORE" comment at line 79 indicates incomplete thought

- [ ] **Lines 81-85 (LIMITATION callout)** - Weak stress position in callout
  - Current: "...or optimize the automation-human interaction trade-off with provable safety bounds."
  - Issue: Ends with least important item (optimization < verification < mathematical guarantees)
  - Fix: "...verify timing properties formally, or provide mathematical guarantees across mode transitions."

- [ ] **Lines 94-97** - Statistics presentation
  - Current: "Multiple independent analyses converge on a striking statistic: \\textbf{70--80\\% of all nuclear power plant events..."
  - Issue: Good use of bold for key statistics. Consider whether all statistics need similar treatment for consistency
  - Note: Lines 100, 119, 125-126 have more statistics—ensure consistent emphasis treatment

- [ ] **Lines 97-99** - Very strong claim, good stress position
  - Current: "...the International Atomic Energy Agency concluded that \"human error was the root cause of all severe accidents at nuclear power plants\"---a categorical statement..."
  - This is excellent—emphatic claim in stress position with proper emphasis

- [ ] **Lines 108-121 (TMI paragraph)** - Generally strong narrative
  - Good use of specific timeline and technical detail
  - Line 119: "\\textbf{44\\% of the fuel melting}" - good emphasis
  - Line 118: "core quickly began to overheat" - could be more specific: "core began overheating within minutes" or similar

- [ ] **Lines 122-143** - Technical paragraph with many statistics
  - Dense paragraph with HRA methods, HEPs, performance shaping factors
  - Line 128: "%%%SOURCE???" indicates missing citation
  - Lines 131-132: Bold statistics are effective
  - Lines 136-142: Many bolded numbers—ensure not overusing bold
  - Overall structure is good but very dense

- [ ] **Lines 145-153** - Rasmussen taxonomy paragraph
  - Good integration of cognitive psychology
  - Line 151: "%%%WHAT IS A CHUNK?" indicates need for brief explanation
  - Consider adding: "(a 'chunk' is a unit of information that can be held as a single entity in working memory)"

- [ ] **Lines 154-163 (LIMITATION callout)** - Very strong
  - This limitation statement is one of the best—specific, well-supported, emphatic
  - No changes needed

### 2.2 Paragraph-Level Issues

- [ ] **Lines 13-34 (Operator role paragraph)** - Break into two paragraphs
  - Current: One long paragraph covering operator qualifications AND paradoxical role with TMI example
  - Issue: Two distinct points being made
  - Fix: Break after line 19 (end of qualification/staffing discussion) before starting paradox discussion (line 21)

- [ ] **Lines 36-61 (Procedures paragraph)** - Very long, multiple sub-topics
  - Current: Covers (1) procedure hierarchy, (2) development process, (3) lack of verification
  - Issue: 26 lines is too long for reader attention span
  - Fix: Break into two paragraphs:
    - Para 1: Procedure hierarchy and development (lines 36-46)
    - Para 2: Lack of formal verification (lines 47-51, then LIMITATION box)

- [ ] **Lines 88-107 (Human factors intro paragraph)** - Dense but well-structured
  - Opens with strong point-issue structure
  - Provides multiple converging lines of evidence
  - Could potentially break after line 102 (end of statistics) before starting specific analysis (line 103), but current structure works

- [ ] **Lines 108-121 (TMI narrative)** - Excellent storytelling
  - Clear chronological structure
  - Specific technical details
  - Builds to climax (44% fuel melting)
  - No changes needed

- [ ] **Lines 122-143 (HRA methods paragraph)** - Very dense
  - Topic: HRA methods and quantitative error rates
  - Issue: Many numbers and concepts in rapid succession
  - Consider: Could break after line 133 (end of nominal rates) before starting performance shaping factors (line 135)

### 2.3 Content and Organization Issues

- [ ] **Section length** - 358 lines, longest in proposal
  - Issue: Risk of reader fatigue/losing track of argument
  - Recommendation: Consider whether all detail is necessary, or if some could move to appendix
  - Specifically: HARDENS subsection (lines 165-295) is 131 lines—nearly as long as entire Research Approach section

- [ ] **HARDENS subsection structure** - Well-organized but very detailed
  - Four sub-subsections: Feasibility Demonstrated (23 lines), Methods Toolkit (42 lines), Discrete Limitation (33 lines), Validation Gap (33 lines)
  - Issue: While all interesting, does the proposal need this much detail on HARDENS?
  - Recommendation: Consider condensing or restructuring to focus more on the gap you're filling rather than recounting HARDENS accomplishments
  - Current structure spends 65 lines on what HARDENS did well, 66 lines on limitations. Could reverse this proportion.

- [ ] **"Research Imperative" subsection (296-358)** - Excellent synthesis but placement
  - Content: Strong synthesis of three converging lines of evidence
  - Issue: This feels like it belongs at the START of Research Approach section rather than end of SOTA
  - Current: SOTA → lists problems → Research Imperative → Research Approach → here's what we'll do
  - Alternative: SOTA → lists problems → Research Approach starts with Imperative → here's what we'll do
  - Consider: Moving lines 296-358 to open Research Approach section

- [ ] **LIMITATION callouts** - Excellent framing device
  - Used consistently throughout: lines 53-60, 81-85, 154-163, 254-263, 287-294
  - These are very effective at signaling gaps
  - Minor: Ensure consistent formatting (all bold, all italic "LIMITATION:")

- [ ] **Transition from Current Practice to HARDENS** - Could be smoother
  - Line 165 starts "The High Assurance Rigorous Digital Engineering..." abruptly
  - Consider adding transition sentence: "Recent work demonstrates that formal methods can address some of these challenges. The High Assurance..."

### 2.4 State of the Art Section - Additional Issues

- [ ] **Lines 165-173 (HARDENS intro)** - Opening could be tighter
  - Current: Two sentences introducing HARDENS, second describes it as "most advanced application...and simultaneously reveals the critical gaps"
  - Issue: "Simultaneously reveals gaps" is your framing, not inherent to HARDENS
  - Fix: "...represents the most advanced application of formal methods to nuclear control systems to date. As we will show, it also illuminates the critical gaps that remain."

- [ ] **Lines 175-181 (HARDENS motivation)** - Good context
  - Explains the problem HARDENS addressed
  - No major issues

- [ ] **Lines 182-190** - Statistics on accomplishment
  - Line 185-186: "\\textbf{nine months at a tiny fraction of typical control system costs}" - good emphasis
  - Consider: "at a tiny fraction" is vague. If you have even rough numbers, use them: "at less than 10% of typical costs" or similar

- [ ] **Lines 192-198 (Kiniry and methodology)** - Dense paragraph
  - Introduces PI, methodology, digital twins, fidelity
  - Many concepts in quick succession
  - Consider: This could be two paragraphs—one on Kiniry/team, one on methodology

- [ ] **Lines 200-231 (Comprehensive toolkit subsection)** - Very detailed
  - Lists many tools: Lando, SysMLv2, FRET, SAT, SMT, Cryptol, SAW, Frama-C, Yosys
  - Issue: Readers may get lost in the tool list and miss the key point
  - Consider: Leading with the key point, then briefly listing tools as support
  - Current: "HARDENS employed impressive array..." → lists tools
  - Alternative: "HARDENS demonstrated complete verification from requirements to implementation [key point], using an impressive array of tools including..."

- [ ] **Lines 207-210** - Bolded text for emphasis
  - "\\textbf{consistency, completeness, and realizability}" - good
  - "\\textbf{complete formal verification from requirements to implementation is technically feasible}" - excellent key claim, right emphasis

- [ ] **Lines 232-263 (Critical Limitation subsection)** - Very strong
  - Clear statement of limitation (discrete only, no continuous)
  - Specific enumeration of what was/wasn't covered
  - Strong LIMITATION callout
  - This is excellent and no changes needed

- [ ] **Lines 265-294 (Validation Gap subsection)** - Clear and specific
  - Explains TRL limitation
  - Lists what wasn't done
  - Good LIMITATION callout
  - Minor: Some repetition between paragraph text and LIMITATION box

### 2.5 State of the Art Section - Sentence-Level Continued

- [ ] **Line 296-311 (Research Imperative opening)** - Strong synthesis
  - "Three converging lines of evidence" is excellent framing
  - Three paragraphs parallel each other well
  - Consider: These three paragraphs are quite dense—each could potentially be broken into smaller units

- [ ] **Lines 302-309** - Weak stress position
  - Current: "Despite extensive regulatory frameworks developed over six decades, \\textbf{no mathematical guarantees exist} that current control approaches maintain safety under all possible scenarios."
  - Issue: Actually good—ends with the key claim (no mathematical guarantees)
  - The bold emphasis helps, but could still be stronger: "...six decades of extensive regulatory frameworks. Yet \\textbf{no mathematical guarantees exist}..."

- [ ] **Lines 312-322** - Another dense summary paragraph
  - Synthesizes human factors argument
  - Many numbers cited: 70-80%, 7±2, 0.001-0.01, 0.1-1.0
  - Strong final sentence: "These limitations \\textbf{cannot be overcome through human factors improvements alone}."

- [ ] **Lines 324-335** - HARDENS summary paragraph
  - Recaps accomplishments and gaps
  - Final sentence is key: "These limitations directly define the research frontier: \\textbf{formal synthesis of hybrid controllers that provide mathematical safety guarantees...}"
  - Very strong, good emphasis

- [ ] **Lines 336-358 (Final "opportunity" paragraph)** - Long but powerful
  - 23 lines synthesizing the argument
  - Strong technical detail
  - Ends well: "compelling and timely research opportunity"
  - Consider: Could break after line 346 (end of problem statement) before starting solution (line 347 "Hybrid control synthesis offers...")

---

## 3. Research Approach Section

### 3.1 Sentence-Level Issues

- [ ] **Lines 3-6** - Weak stress position in opening sentence
  - Current: "This research will overcome the limitations of current practice to build high-assurance hybrid control systems for critical infrastructure."
  - Issue: Ends with "critical infrastructure"—generic and expected
  - Fix: "This research will build high-assurance hybrid control systems by overcoming current practice limitations."

- [ ] **Lines 6-14** - Equations introduced clearly
  - Good contextualization of equations (hybrid = continuous + discrete)
  - Minor: Lines 16-17 have $f(\cdot)$ and $\nu(\cdot)$ explanations that could reference equation numbers

- [ ] **Lines 19-20** - Topic position could be smoother
  - Current: "Our focus centers on continuous autonomous hybrid systems..."
  - Previous sentence discusses "control input $u$"
  - Could connect better: "Within this hybrid framework, we focus on continuous autonomous systems..."

- [ ] **Line 23** - Example is good but could be emphasized
  - Current: "For example, a nuclear reactor switching from warm-up to load-following control cannot instantaneously change its temperature or control rod position, but can instantaneously change control laws."
  - Issue: Key insight (continuous states unchanged, discrete transitions instant) could be more prominent
  - Fix: "Physical systems exhibit this property naturally: a nuclear reactor switching from warm-up to load-following control changes control laws instantly, but its temperature and control rod position evolve continuously."

- [ ] **Lines 26-28** - Good framing of three thrusts
  - Clear enumeration
  - No major issues

- [ ] **Lines 30-38** - Enumeration formatting
  - Using \\begin{enumerate} is good
  - Items are parallel in structure
  - Consider: Items 1-2 are short (one line), item 3 is longer (two lines). Could make more parallel by expanding 1-2 slightly

- [ ] **Lines 40-41** - Weak metadiscourse
  - Current: "The following sections discuss how these thrusts will be accomplished."
  - Issue: Pure metadiscourse, provides no information
  - Fix: Delete entirely, or combine with previous: "...we must accomplish three main thrusts, each detailed below:"

### 3.2 Research Approach - Subsection 1 (Procedures → Temporal Logic)

- [ ] **Lines 42** - Subsection title uses math notation
  - Current: "$(Procedures \wedge FRET) \rightarrow Temporal Specifications$"
  - Issue: Clever but potentially unclear. Not all readers will parse this as "Procedures AND FRET implies Temporal Specs"
  - Consider: Adding plain-English subtitle: "Translating Procedures into Temporal Logic"

- [ ] **Lines 44-49** - Opening paragraph point could be sharper
  - Current: "The motivation behind this work stems from the fact that commercial nuclear power operations remain manually controlled..."
  - Issue: "The motivation behind this work" is weak opening. More direct: "Commercial nuclear power operations remain manually controlled despite advances in control systems. However, operators follow highly prescriptive, well-documented procedures—suggesting that autonomous control is technically feasible."

- [ ] **Lines 51-55** - Good clear claim
  - "Written procedures and requirements...are sufficiently detailed that we may be able to translate them into logical formulae with minimal effort."
  - This is a strong claim and key assumption
  - Consider: "Minimal effort" may overstate—later sections describe significant work in FRET formalization
  - Fix: "...that we can systematically translate them into logical formulae."

- [ ] **Lines 60-68** - SCRAM example is excellent
  - Specific natural language requirement
  - Translation to temporal logic with explanation
  - Clear equation formatting
  - Consider: This is a model for what examples should look like

- [ ] **Lines 70-75** - Explanation of operators
  - Good: Explains what $G$, $X$, $U$ mean in context
  - Helps readers unfamiliar with temporal logic

- [ ] **Lines 76-81** - FRET introduction
  - Clear motivation for why FRET
  - Could be slightly tighter: "The most efficient path to accomplish this translation is through NASA's Formal Requirements Elicitation Tool (FRET)"
  - Consider: "Most efficient" is a strong claim. Have you compared alternatives? If not, soften: "NASA's FRET provides a systematic path for this translation"

- [ ] **Lines 83-93 (FRET six components)** - Clear enumeration
  - Parallel structure
  - Good use of italics for questions
  - Line 84: "%CITE FRET MANUAL" - needs citation
  - Minor: Some items very short (line 90 just "Shall"), others longer. Consider whether parallel structure could be tighter

- [ ] **Lines 95-110** - Realizability paragraph
  - Opens with strong point: "FRET provides functionality to check the *realizability*..."
  - Explains what realizability means
  - Makes clear argument for why this matters (finding bugs early)
  - Structure is good

- [ ] **Lines 105-110** - Second category of realizability
  - Discusses undefined behaviors
  - Good point about autonomous controllers needing complete specifications
  - Line 107-108: "This ambiguity is undesirable for high-assurance systems, since even well-trained humans remain prone to errors" - good connection back to human factors from SOTA

- [ ] **Lines 112-115** - Closing/transition
  - States that FRET exports to synthesis tools
  - Good transition to next subsection
  - Line 114-115: "progression to the next step of our approach" - could be more specific about what that next step is

### 3.3 Research Approach - Subsection 2 (Temporal Logic → Discrete Automata)

- [ ] **Line 117** - Subsection title again uses math notation
  - Same issue as line 42
  - Consider adding plain-English subtitle

- [ ] **Lines 119-122** - Opening defines reactive synthesis
  - Good clear definition
  - "Active research field" - consider whether you need to say this. It's clear from the work that this is active research.

- [ ] **Lines 123-133** - Description of automata
  - Explains finite states, transitions, etc.
  - Good pedagogical approach
  - Lines 131-132: "Hybrid systems naturally exhibit discrete behavior amenable to formal analysis through these finite state representations" - this is a key claim and could be more prominent

- [ ] **Lines 135-143** - Strix tool and implementation
  - Good specific tool choice with justification (SYNTCOMP performance)
  - Lines 138-139: "maximizing generated automata quality" - what does quality mean here? Minimal states? Interpretability? Could be more specific
  - Lines 140-143: Implementation discussion is good—notes that automaton provides communication path to programmers without formal methods expertise

- [ ] **Lines 145-158** - Why discrete automata / correctness argument
  - This paragraph makes the key argument for correct-by-construction
  - Strong rhetorical structure: "because X, we can prove Y"
  - Lines 150-154: Comparison with human operators is effective
  - Lines 155-158: "By synthesizing controllers from logical specifications with guaranteed correctness, we eliminate the possibility of switching errors" - very strong claim, worth emphasizing

- [ ] **Line 158** - Ends with strong claim
  - "...we eliminate the possibility of switching errors."
  - Excellent stress position—key contribution
  - Consider: Adding emphasis (bold or italics) to this claim

### 3.4 Research Approach - Subsection 3 (Continuous Modes)

- [ ] **Lines 160-161** - Subsection title
  - Again uses math notation
  - This one is longer: "$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$"
  - Consider plain-English subtitle

- [ ] **Lines 163-168** - Opening paragraph
  - Good point that discrete is only half
  - Refers back to equation 1 (good callback)
  - States section purpose clearly

- [ ] **Lines 170-176** - Continuous modes after discrete
  - Explains why discrete comes first
  - "Physics-agnostic specifications" is good phrase
  - Rationale is clear

- [ ] **Lines 177-208** - Three-mode classification
  - **This is a key contribution and should be highlighted more prominently**
  - Current: Presented as straightforward categorization
  - Issue: This is novel! Stabilizing/Transitory/Expulsory framework is your innovation
  - Fix: Add sentence before enumeration: "We propose a three-mode classification based on discrete transition structure. This taxonomy enables systematic continuous controller design tailored to each mode's objectives."

- [ ] **Lines 183-189 (Stabilizing mode)** - Clear definition
  - Good explanation with example
  - "Nodes with only incoming transitions" is clever—shows how discrete structure determines continuous requirements

- [ ] **Lines 191-197 (Transitory mode)** - Clear definition
  - Good explanation
  - Minor: "Secondary objectives" (line 195)—could clarify with example

- [ ] **Lines 199-207 (Expulsory mode)** - Clear definition
  - Good emphasis on safety constraints
  - SCRAM example is excellent
  - This definition is slightly longer than the other two—appropriate given importance

- [ ] **Lines 209-221** - Why build continuous after discrete
  - Makes clear argument for the approach
  - "Local controller design focused on satisfying discrete transitions" - key insight
  - Lines 213-214: "Current techniques struggle...because dynamic discontinuities complicate verification" - good problem statement
  - Lines 214-221: Explains how your approach avoids this problem

- [ ] **Lines 220-221** - Introduces three techniques
  - "To ensure continuous modes satisfy their requirements, we will employ three main techniques..."
  - Good signposting
  - Note: "employ" again—consider "use" or restructure to make techniques the subject

- [ ] **Lines 223-232 (Reachability Analysis)** - Clear explanation
  - Defines technique
  - States what it's used for
  - Mentions recent advances (neural networks for Hamilton-Jacobi)
  - Well-structured

- [ ] **Lines 234-240 (Assume-Guarantee Contracts)** - Clear explanation
  - Explains compositional approach
  - Shows how contracts enable local analysis
  - Minor: Line 234 says "will be employed"—passive. Fix: "We will use assume-guarantee contracts..." or "Assume-guarantee contracts enable..."

- [ ] **Lines 242-249 (Barrier Certificates)** - Clear explanation
  - Explains what they prove
  - Gives specific example
  - Technical detail (differential inequality conditions) is appropriate
  - Well-structured

- [ ] **Lines 250-273 (SmAHTR demonstration)** - Excellent specificity
  - This paragraph provides concrete detail: SmAHTR, Simulink model, Emerson Ovation, ARCADE
  - Multiple sentences are quite long (lines 252-260 is 60+ words, lines 261-271 is 73 words)
  - Consider breaking these into shorter sentences for readability

- [ ] **Lines 275-289 (Concluding paragraph)** - Strong synthesis
  - "Unified approach" language is good
  - Connects back to gap from SOTA
  - Final sentence (lines 285-289) is long (66 words) but well-structured
  - Ends strongly: "...domain where operating procedures are well-documented and safety is paramount."

- [ ] **Lines 290-296** - Comments for future revision
  - These should be removed from final version
  - But they're good notes: figures, validation approach, examples
  - Consider whether any should be addressed before submission

### 3.5 Research Approach - Paragraph-Level Issues

- [ ] **Opening paragraph (lines 3-24)** - Could be split
  - Current: Covers (1) overcoming limitations, (2) equations, (3) focus on continuous autonomous systems, (4) example
  - Issue: Four distinct sub-topics in one paragraph
  - Consider: Breaking after line 14 (after equations) or after line 20 (after focus statement)

- [ ] **Three-thrust framing (lines 26-38)** - Good structure
  - Clear signposting
  - Enumeration is parallel
  - Consider: The metadiscourse sentence (lines 40-41) could be deleted or moved to introduction

- [ ] **FRET component enumeration (lines 86-93)** - Could be formatted better
  - Currently as enumeration which is good
  - But questions in italics could be formatted more consistently
  - Consider: Making all questions boldface or using a different structure

### 3.6 Research Approach - Content Issues

- [ ] **Three-mode classification prominence** - Underemphasized
  - This appears to be a novel contribution
  - Currently presented as straightforward categorization
  - Should be highlighted as key methodological innovation
  - Consider: Adding sentence like "This classification, to our knowledge, has not been systematically applied to hybrid control synthesis before."

- [ ] **Tool choices** - Well justified
  - FRET: choice is well-motivated
  - Strix: justified by SYNTCOMP performance
  - Reachability, barrier certificates: standard techniques
  - No issues

- [ ] **Level of technical detail** - Appropriate
  - Enough detail to demonstrate feasibility
  - Not so much that non-experts are lost
  - Good balance

- [ ] **Examples** - Excellent
  - SCRAM requirement (line 60) - very specific
  - Load-following controller (line 187) - clear
  - Warm-up procedure (line 193) - clear
  - SCRAM as expulsory mode (line 203) - powerful callback

---

## 4. Metrics of Success Section

### 4.1 Sentence-Level Issues

- [ ] **Lines 3-8** - Opening paragraph
  - States TRL approach clearly
  - Line 6: "This section explains why TRL advancement provides..." - metadiscourse could be tighter
  - Fix: Delete line 6-8 (metadiscourse) or combine: "Technology Readiness Levels provide the ideal metric, measuring both..."

- [ ] **Lines 10-19** - TRL justification paragraph 1
  - Makes argument for why TRLs
  - Multiple short sentences with parallel structure
  - Effective rhetoric
  - Line 16-17: "This gap is precisely what this work aims to bridge" - good, but "this work" could be "we aim"

- [ ] **Lines 21-31** - TRL justification paragraph 2
  - Continues argument
  - Good points about nuclear industry requirements
  - Lines 29-31: Weak stress position - ends with "publications alone cannot" (negative)
  - Fix: "...making this metric directly relevant to potential adopters and clearly demonstrating feasibility and maturity."

- [ ] **Lines 32-39** - Current/target TRL
  - Clear statement of starting point and goal
  - Good signposting: "Moving from current state to target requires..."
  - Minor: "Early TRL 3" (line 35)—is "early" necessary? Could just say "TRL 3"

- [ ] **Lines 41-49 (TRL 3 definition)** - Clear and specific
  - Paragraph format beginning with "\\paragraph{TRL 3...}" is good
  - Specific criteria listed
  - Line 43: "For this research, TRL 3 means..." - clear personalization
  - Good structure

- [ ] **Lines 51-60 (TRL 4 definition)** - Clear and specific
  - Similar structure to TRL 3, which is good
  - Specific criteria
  - "Zero safety violations" (line 59) - good concrete metric

- [ ] **Lines 62-78 (TRL 5 definition)** - Longest and most detailed
  - Appropriate given it's the target
  - Lines 71-76: Discussion of off-nominal scenarios is good
  - Line 73-74: "Graded responses to minor disturbances are outside the scope" - good explicit scoping statement
  - Minor: Could potentially break into two paragraphs—one on hardware (lines 62-70), one on validation (lines 70-78)

- [ ] **Lines 80-83** - Synthesis of TRL progression
  - "These levels define progressively more demanding demonstrations" - good summary
  - Three parallel statements: "TRL 3 proves..., TRL 4 proves..., TRL 5 proves..." - effective
  - Could be even more parallel: "TRL 3 proves individual components work. TRL 4 proves they integrate in simulation. TRL 5 proves they run on industrial hardware."

- [ ] **Lines 85-96** - Quarterly assessment and revision criteria
  - Long paragraph covering two topics: (1) progress assessment, (2) revision triggers
  - Consider breaking after line 89 (end of assessment discussion) before starting revision discussion (line 90)
  - Lines 91-94: Three specific failure modes listed - good concrete triggers

### 4.2 Paragraph-Level Issues

- [ ] **Lines 10-31** - Two TRL justification paragraphs
  - Issue: These two paragraphs both argue why TRLs are appropriate
  - Could be combined into single tighter paragraph
  - Current word count: ~160 words across two paragraphs
  - Fix: Combine key points into one paragraph (~120 words), make argument more concise

- [ ] **TRL definitions (lines 41-78)** - Three paragraphs in parallel structure
  - Excellent parallelism
  - Each uses "For this research, TRL X means..."
  - Each lists specific criteria
  - Each ends with "This proves..."
  - This is very effective and should be maintained

- [ ] **Lines 98-105** - Success statement
  - Opens with clear claim: "This research succeeds if..."
  - Explains why this demonstrates success
  - Good closing paragraph for section

### 4.3 Metrics Section - Content Issues

- [ ] **Justification for TRLs** - Somewhat defensive tone
  - Two paragraphs (lines 10-31) justifying why TRLs are appropriate
  - While argument is sound, the length suggests defensiveness
  - Consider: Could this be condensed to make it feel less defensive?
  - Alternative: Perhaps reviewers have questioned TRL approach in past? If so, this is appropriate.

- [ ] **Measurability** - Excellent
  - Each TRL has concrete, measurable criteria
  - "Fewer than 1,000 states" (line 77)
  - "Zero safety violations across 100 consecutive runs" (line 93)
  - This specificity is excellent

- [ ] **Quarterly assessment** - Good accountability
  - Shows you've thought about project management
  - Revision criteria show you've thought about failure modes
  - This strengthens the proposal

---

## 5. Risks and Contingencies Section

### 5.1 Sentence-Level Issues

- [ ] **Lines 3-12** - Opening paragraph
  - Good overview structure
  - Line 9: "Each risk has associated indicators for early detection" - good framing
  - Line 11-12: "The staged project structure ensures..." - passive. Fix: "Our staged project structure ensures..."

- [ ] **Lines 14-24** - Computational tractability risk statement
  - Clear problem statement
  - Lines 17-21: Long sentence (51 words) with complex structure
  - Consider breaking after "specification complexity" or "state"
  - Fix: "Reactive synthesis scales exponentially with specification complexity, which creates risk of intractable synthesis times. Temporal logic specifications from complete startup procedures may produce automata with thousands of states, requiring days or weeks of synthesis time. This would prevent demonstrating the complete methodology within project timelines."

- [ ] **Lines 26-35** - Indicators paragraph
  - Good concrete indicators
  - Parallel structure: "X would suggest Y", "X would indicate Y", etc.
  - Effective

- [ ] **Lines 37-45** - Contingency plan
  - Clear fallback
  - Specific scope reduction described
  - Line 42: "The research contribution would remain valid" - good positive framing
  - Line 44-45: "constraint rather than a failure" - excellent reframing

- [ ] **Lines 47-54** - Time-scale separation mitigation
  - Technical depth is good
  - Shows sophisticated understanding
  - Minor: Line 48: "can be treated quasi-steady" - may be jargon for some readers. Consider: "can be approximated as steady"

- [ ] **Lines 56-63** - Access to HPC resources
  - Good mention of available resources
  - Shows preparedness
  - Line 59: "high-performance computing resources" - first mention of CRC facility (it was in budget)

### 5.2 Discrete-Continuous Interface Section

- [ ] **Lines 65-79** - Problem statement
  - Clear explanation of fundamental challenge
  - Long sentences (lines 72-78 is 57 words)
  - Consider breaking: "Temporal logic operates on boolean predicates, while 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."

- [ ] **Lines 81-92** - Indicators
  - Parallel structure: "X would suggest Y", "X would indicate Y"
  - Good technical specificity
  - Line 84-85: "Boolean abstraction" appears twice (lines 73 and 84) - be consistent with terminology

- [ ] **Lines 94-107** - Polytopic invariants contingency
  - Technical and specific
  - Good explanation of what polytopes are and why they help
  - Line 100: "inner-approximated" - good use of precise term, but consider whether definition needed
  - Lines 103-107: Shows you've already thought about this in your three-mode classification

- [ ] **Lines 109-119** - Mitigation strategies
  - "Design-for-verification" (line 113) is good concept
  - Control barrier functions mentioned again (callback to Research Approach)
  - Shows integrated thinking

### 5.3 Procedure Formalization Section

- [ ] **Lines 121-134** - Problem statement
  - Clear explanation of challenge
  - Good point about procedures written for humans with contextual understanding
  - Lines 131-134: Risk is framed positively - "not merely that formalization is difficult, but that current procedures fundamentally lack the precision required"

- [ ] **Lines 136-148** - Indicators
  - Good concrete indicators
  - Line 141-142: References to "operator judgment" in procedures - very specific and realistic
  - Line 145-148: "Domain experts unable to provide crisp answers" - excellent indicator

- [ ] **Lines 150-163** - Contingency as contribution
  - Excellent reframing: documentation of gaps is itself valuable
  - "Taxonomy of formalization barriers" (line 152) - good concept
  - Lines 156-160: Shifts from "here's a controller" to "here's what's needed"—good pivot
  - This contingency is particularly well-developed

- [ ] **Lines 165-177** - Mitigation strategies
  - Early engagement with domain experts
  - Cross-design comparison
  - Both are good strategies showing preparedness

### 5.4 Hardware-in-Loop Integration Section

- [ ] **Lines 179-190** - Problem statement
  - Clear technical challenges listed
  - Specific timing requirements mentioned (10-100 Hz)
  - Good detail level

- [ ] **Lines 192-203** - Indicators
  - Specific technical indicators (dropouts, buffer overruns, computational limits)
  - Good progression from communication → computation → timing

- [ ] **Lines 205-218** - Software-in-loop contingency
  - Good fallback that maintains TRL 4
  - Explains why this still demonstrates value
  - Line 214-217: "research contribution remains intact" - good positive framing
  - Note this maintains TRL 4 not TRL 5 (appropriate scoping)

- [ ] **Lines 220-232** - Mitigation strategies
  - ARCADE prior success mentioned
  - Early testing recommended
  - Ovation flexibility noted
  - All show preparedness

### 5.5 Risks Section - Paragraph-Level Issues

- [ ] **Four main subsections** - Well-balanced structure
  - Each has: (1) problem statement, (2) indicators, (3) contingency, (4) mitigation
  - Parallel structure is effective
  - Lengths: Computational (48 lines), Discrete-Continuous (58 lines), Procedure (58 lines), HIL (54 lines)
  - Fairly balanced

- [ ] **Opening paragraph** - Could be tighter
  - Lines 3-12: Sets up structure
  - Could potentially be combined with subsequent topic sentences
  - But current structure works

### 5.6 Risks Section - Content Issues

- [ ] **Risk selection** - Comprehensive
  - Four major risks cover computational, theoretical, practical/procedural, and implementation
  - Good coverage of different risk categories

- [ ] **Contingency quality** - Excellent
  - Each contingency preserves value
  - Scope reductions are reasonable
  - Positive framing ("contribution" not "failure")

- [ ] **Indicators specificity** - Very good
  - Concrete, measurable indicators
  - Early warning focus
  - This shows project management maturity

- [ ] **Balance of subsections** - Good
  - Roughly equal length
  - But: is length proportional to actual risk magnitude?
  - Discrete-continuous interface seems most fundamental, but doesn't get more space
  - Consider: Does space allocation reflect importance, or just complexity of explanation?

---

## 6. Broader Impacts Section

### 6.1 Sentence-Level Issues

- [ ] **Lines 3-10** - Opening paragraph
  - Good hook: AI datacenters renewing SMR interest
  - Clear problem setup
  - Line 8-9: "However, the economics of nuclear power deployment at this scale demand careful attention to operating costs" - somewhat cautious phrasing
  - Consider: "However, nuclear power economics depend critically on reducing operating costs"

- [ ] **Lines 12-23** - Economic statistics paragraph
  - Excellent use of specific numbers
  - $88.24/MWh, 1,050 TWh, $92B annually, 23-30% for O&M
  - This level of specificity is persuasive
  - Minor: Long sentences (lines 18-23 is 54 words)
  - Consider breaking after "$92 billion": "...cost of power generation would exceed $92 billion. Within this figure, operations and maintenance represents..."

- [ ] **Lines 25-37** - How research addresses costs
  - Clear connection: autonomous control → reduced staffing → lower O&M
  - Good explanation of staffing challenge for SMRs
  - Lines 30-33: Long sentence (48 words) could be broken

- [ ] **Lines 38-50** - Correct-by-construction importance
  - Good argument for why formal methods matter
  - Explains what automation can/can't do (routine vs. off-normal)
  - Line 49-50: "much cheaper to operate" - consider whether more precise language available

- [ ] **Lines 52-62** - SMR deployment paragraph
  - Good connection: NRC certification documents → FRET → synthesis
  - "Infrastructure of requirements and specifications is already complete as part of licensing process" (lines 59-61) - this is a key insight and could be more prominent

- [ ] **Lines 64-74** - Generalization paragraph
  - Good broader impact: methodology generalizes
  - Lists other domains (chemical, aerospace, transportation)
  - Lines 71-74: Long final sentence (43 words) - consider breaking

### 6.2 Paragraph-Level Issues

- [ ] **Section length** - At 75 lines, this is the briefest technical section
  - Issue: Given that economic motivation is central to SMRs, this could be expanded
  - Missed opportunities: workforce development, educational impacts, equity considerations

- [ ] **Paragraph structure** - Generally good
  - Seven paragraphs covering: (1) context, (2) economics, (3) how research helps, (4) why formal methods, (5) SMR fit, (6) generalization
  - Logical flow

### 6.3 Broader Impacts - Content Issues

- [ ] **Economic analysis** - Excellent
  - Specific numbers
  - Clear chain: electricity cost → total demand → O&M costs
  - This is persuasive

- [ ] **Missing elements** - Several
  - **Workforce/educational impacts**: Training engineers in formal methods, developing curriculum, broader CS-engineering integration
  - **Equity considerations**: Clean energy access, distributed generation benefits
  - **International implications**: Methodology could help other countries deploy SMRs
  - **Environmental justice**: How does autonomous control affect siting near communities?
  - Not all needed, but one or two would strengthen section

- [ ] **Generalization** - Good but brief
  - Lists domains (chemical, aerospace, transportation)
  - Could expand slightly: What specific applications? Pipeline safety? Aircraft control? Autonomous vehicles?

---

## 7. Budget Section (Brief Review)

As requested, this section receives lighter treatment focusing on major issues only.

### 7.1 Major Issues

- [ ] **Line 73** - Typo
  - "t ranslation" should be "translation"

- [ ] **Table formatting** - Appears correct
  - Budget table uses booktabs style (good)
  - Numbers align properly
  - Categories are clear

- [ ] **High-performance workstation** - Consider upgrade path
  - Year 1: $3,500 for workstation
  - Years 2-3: No upgrades budgeted
  - Issue: As synthesis scales up, might need more compute
  - Consider: Adding small line item for upgrades/expansion in Years 2-3?

- [ ] **Software note (lines 191-197)** - Good
  - Explicitly states all software is free/licensed
  - ARCADE through partnership
  - This prevents questions

- [ ] **In-kind contributions (lines 250-277)** - Well-documented
  - Emerson partnership valued
  - University contributions noted
  - Total estimated at $20,000+
  - Good to document this explicitly

### 7.2 Budget Section - Overall Assessment

- Budget is comprehensive, well-justified, and appropriate
- Fringe benefit rates are clearly stated
- Travel budget is reasonable
- No major concerns

---

## 8. Schedule Section (Brief Review)

As requested, this section receives lighter treatment focusing on major issues only.

### 8.1 Major Issues

- [ ] **Line 73** - Spacing issue
  - "t ranslation methodology" has incorrect space
  - Should be "translation methodology"

- [ ] **Gantt chart** - Appears well-structured
  - Overlapping tasks shown appropriately
  - Milestones marked clearly
  - Publications timeline shown

- [ ] **Publication strategy (lines 115-141)** - Excellent
  - Explains venue choices
  - NPIC&HMIT for nuclear community
  - IEEE TAC for control theory community
  - Rationale for each is clear
  - Builds on prior success (best student paper)

### 8.2 Schedule Section - Overall Assessment

- 24-month timeline is ambitious but realistic
- Six trimesters for dissertation is reasonable
- Milestone structure aligns with TRL progression
- No major concerns

---

## 9. Big Picture Issues

### 9.1 Cross-Cutting Issues

- [ ] **Three-mode classification** - Novel contribution underemphasized
  - Location: Research Approach, lines 178-208
  - Issue: This stabilizing/transitory/expulsory framework appears to be novel, but is presented as routine categorization
  - Impact: You may not be getting credit for this innovation
  - Fix: Explicitly state novelty: "We propose a three-mode classification for hybrid control design. To our knowledge, this systematic taxonomy has not previously been applied to hybrid control synthesis."
  - Cross-reference: This should be mentioned in Goals section as one of the methodological contributions

- [ ] **Discrete-continuous interface verification** - Key contribution
  - Location: Research Approach subsection 3
  - Issue: The unified verification across discrete-continuous interface is your main contribution, but this isn't always explicit
  - Impact: Reviewers may not fully appreciate novelty
  - Fix: In Goals section, explicitly state: "The key innovation is unified verification across the discrete-continuous interface—ensuring both switching logic and continuous dynamics are provably correct."

- [ ] **SmAHTR introduction timing** - Appears abruptly
  - Location: First mentioned in Goals (line 92), detailed in Research Approach (line 253)
  - Issue: SmAHTR suddenly appears as the demonstration case without build-up
  - Fix: Introduce SmAHTR earlier, perhaps in Goals section: "We will demonstrate this methodology by developing an autonomous startup controller for a Small Modular Advanced High Temperature Reactor (SmAHTR), transitioning from cold shutdown through criticality to full power operation."

### 9.2 Consistency Issues

- [ ] **Terminology consistency** - Generally good
  - "Correct by construction" vs. "provably correct" - used somewhat interchangeably
  - "Hybrid automata" vs. "discrete automata" vs. "finite state automata" - generally clear from context
  - "Reachability analysis" - consistent usage
  - No major inconsistencies

- [ ] **Notation consistency** - Good
  - $f(\cdot)$ and $\nu(\cdot)$ introduced clearly
  - Temporal logic operators ($G$, $X$, $U$, $F$) explained when introduced
  - Mathematical notation is consistent

- [ ] **Section cross-references** - Could be stronger
  - SOTA identifies gaps → Research Approach should explicitly reference these
  - Current: connections are implicit
  - Fix: In Research Approach opening, add: "This approach addresses the three limitations identified in Section 2: procedures lacking formal verification, current practice treating continuous and discrete separately, and HARDENS verifying discrete logic without continuous dynamics."

### 9.3 Argument Flow

- [ ] **Problem → Solution arc** - Clear and strong
  - Problem: Operators make errors (SOTA human factors section)
  - Gap: No formal verification of procedures or hybrid behavior (SOTA limitations)
  - Solution: Hybrid control synthesis with discrete + continuous verification (Research Approach)
  - Evidence: TRL progression demonstrates feasibility (Metrics)
  - Risks addressed: Comprehensive contingencies (Risks)
  - Impact: Economic viability of SMRs (Broader Impacts)
  - This structure is excellent

- [ ] **"So what" connections** - Could be more explicit
  - Issue: Sometimes you present information without explicitly stating why it matters
  - Examples:
    - After Goals section: Add "If successful, this enables..."
    - Between SOTA and Research Approach: Add "These gaps create an urgent research opportunity"
    - After Metrics section: Add "Achieving TRL 5 would provide a clear path to industrial adoption"

- [ ] **Callbacks and forward references** - Could be stronger
  - Research Approach could reference specific SOTA limitations by name
  - Metrics could reference specific risks
  - Broader Impacts could callback to human factors statistics from SOTA

### 9.4 Missing Elements

- [ ] **Cybersecurity** - Not mentioned
  - Issue: For autonomous nuclear control, cybersecurity is critical
  - Impact: Reviewers may wonder why this isn't addressed
  - Fix: Add brief paragraph (perhaps in Risks section or Research Approach) on security verification
  - Could mention: "While cybersecurity verification is beyond the scope of this phase, the formal methods infrastructure we develop provides a foundation for subsequent security verification using techniques like information flow analysis and secure compilation."

- [ ] **Regulatory path** - Mentioned but not detailed
  - Issue: You mention NRC requirements but don't describe approval process
  - Impact: May seem naive about regulatory challenges
  - Fix: Add paragraph in Broader Impacts discussing regulatory pathway: "NRC Standard Review Plan provides pathways for digital I&C approval (NUREG-0800, Chapter 7). The formal verification artifacts we produce—including provable correctness claims, traceability from requirements to implementation, and systematic testing evidence—align with NRC expectations for high-assurance systems. While full regulatory approval is beyond this research scope, our methodology produces the documentation foundation NRC requires."

- [ ] **ML/AI alternatives** - Not discussed
  - Issue: Machine learning for control is prominent. Why not use ML?
  - Impact: Reviewers may wonder if you've considered alternatives
  - Fix: Add brief paragraph early in Research Approach: "Machine learning approaches to autonomous control have received significant attention. However, neural network controllers are fundamentally black-box systems that cannot provide the mathematical safety guarantees required for nuclear applications. Recent work on verified neural networks shows promise, but the state of the art remains far from the assurance levels nuclear safety demands. Formal methods provide the only currently viable path to provable correctness for safety-critical autonomous control."

### 9.5 Strengths to Maintain

- [ ] **Specific examples** - Excellent throughout
  - TMI accident narrative
  - SCRAM requirement translation
  - HARDENS project detail
  - SmAHTR demonstration
  - These make the proposal concrete and believable

- [ ] **Statistical evidence** - Very strong
  - 70-80% human error rate
  - Economic projections ($92B annually)
  - HEP rates (0.001-0.01 → 0.1-1.0)
  - Specific numbers are persuasive

- [ ] **Technical depth** - Appropriate level
  - Enough detail to demonstrate expertise
  - Not so much that non-experts are lost
  - Good balance for mixed audience

- [ ] **Risk analysis** - Exceptionally thorough
  - Four major risks identified
  - Concrete indicators
  - Viable contingencies
  - Positive framing
  - This is a model for risk sections

---

## Summary Statistics

**Total issues documented**: 150+

**By level**:
- Sentence-level: ~70 issues
- Paragraph-level: ~40 issues
- Content/organization: ~40 issues

**By section**:
- Goals and Outcomes: 18 issues
- State of the Art: 45 issues (longest section, most issues)
- Research Approach: 40 issues
- Metrics of Success: 12 issues
- Risks and Contingencies: 20 issues
- Broader Impacts: 10 issues
- Budget: 3 issues (light review)
- Schedule: 3 issues (light review)
- Big Picture: 10 issues

**Priority levels** (estimated):
- HIGH impact: ~15 issues (major organization, missing content, key contributions underemphasized)
- MEDIUM impact: ~60 issues (sentence-level patterns, paragraph structure, clarity)
- LOW impact: ~75 issues (minor wording, polish, consistency)

---

## Revision Strategy Recommendation

1. **Start with Big Picture issues** (Section 9) - Ensure novel contributions are highlighted
2. **Address Priority Issues 1-5** from Executive Summary
3. **Work section-by-section** using this detailed document
4. **Apply patterns** from Executive Summary to similar cases
5. **Final consistency pass** - Terminology, cross-references, formatting

The proposal has strong technical content and solid structure. These revisions will enhance clarity, emphasize your contributions, and strengthen your argument. Good luck!