diff --git a/2-state-of-the-art/state-of-art.tex b/2-state-of-the-art/state-of-art.tex
index f09ec0f..810224d 100644
--- a/2-state-of-the-art/state-of-art.tex
+++ b/2-state-of-the-art/state-of-art.tex
@@ -1,269 +1,303 @@
 \section{State of the Art and Limits of Current Practice}
 
 The principal aim of this research is to create autonomous reactor control
-systems that are tractably safe. To understand what is being automated, we must
-first understand how nuclear reactors are operated today. This section examines
-reactor operators and the operating procedures we aim to leverage, then
-investigates limitations of human-based operation, and concludes with current
-formal methods approaches to reactor control 
-systems.\splitnote{Good roadmap --- tells reader exactly what's 
-coming.}\dasinline{Don't like ``we'' here. Sounds like
-``we're going on an adventure!'' and feels jocular.
-Maybe: ``To motivate this proposal, the state of
-the art of nuclear reactor control, blah, and blah,
-are discussed in this section.''}
+systems that are tractably safe. \oldt{To understand what is being automated,
+we must first understand how nuclear reactors are operated today. This section
+examines reactor operators and the operating procedures we aim to leverage,
+then investigates limitations of human-based operation, and concludes with
+current formal methods approaches to reactor control systems.}
+\newt{Understanding what is being automated requires understanding how
+nuclear reactors are operated today. This section examines reactor operating
+procedures, investigates limitations of human-based operation, and reviews
+current formal methods approaches to reactor control
+systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
+adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
+state of the art of nuclear reactor control, blah, and blah, are discussed
+in this section.''}
 
 \subsection{Current Reactor Procedures and Operation}
 
-Nuclear plant procedures exist in a hierarchy: normal operating procedures for
-routine operations, abnormal operating procedures for off-normal conditions,
-Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
-Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
-Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
-scenarios.\dasinline{This sentence is MASSIVE. Why is
-there 6 lines describing different types of
-procedures? WHO CARES? Need a sentence after saying
-why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
-developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
-development 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~\cite{10CFR55.59}. Despite this rigor,
-procedures fundamentally lack formal verification of key safety 
-properties.\dasinline{Does the audience know what formal
-verification is at this point? Probably, but should
-say differently. Maybe `exhaustive' or
-`definitive'.} No
-mathematical proof exists that procedures cover all possible plant states, that
-required actions can be completed within available timeframes, or that
-transitions between procedure sets maintain safety 
-invariants.\splitsuggest{This paragraph is doing a lot. Consider splitting: 
-first paragraph on the hierarchy and compliance, second on the lack of formal 
-verification. The ``No mathematical proof exists...'' sentence is powerful and 
-deserves emphasis.}
+\oldt{Nuclear plant procedures exist in a hierarchy: normal operating
+procedures for routine operations, abnormal operating procedures for
+off-normal conditions, Emergency Operating Procedures (EOPs) for
+design-basis accidents, Severe Accident Management Guidelines (SAMGs) for
+beyond-design-basis events, and Extensive Damage Mitigation Guidelines
+(EDMGs) for catastrophic damage scenarios.} \newt{Nuclear plant operations
+are governed by a hierarchy of written procedures, ranging from normal
+operating procedures for routine operations to Emergency Operating
+Procedures (EOPs) for design-basis accidents and Severe Accident Management
+Guidelines (SAMGs) for beyond-design-basis events. These procedures exist
+because reactor operation requires deterministic responses to a wide range
+of plant conditions, from routine power changes to catastrophic
+failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
+describing different types of procedures? WHO CARES? Need a sentence after
+saying why we have these procedures.} These procedures must comply with 10
+CFR 50.34(b)(6)(ii) and are developed using guidance from
+NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies
+fundamentally on expert judgment and simulator validation rather than formal
+verification.
 
-\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
-and completeness.} Current procedure development relies on expert judgment and
-simulator validation. No mathematical proof exists that procedures cover all
-possible plant states, that required actions can be completed within available
-timeframes, or that transitions between procedure sets maintain safety
-invariants. Paper-based procedures cannot ensure correct application, and even
-computer-based procedure systems lack the formal guarantees that automated
-reasoning could provide.\splitpolish{This repeats the ``No mathematical 
-proof exists...'' sentence almost verbatim from the paragraph above. Either 
-cut it from the paragraph or from the LIMITATION box.}
+Procedures undergo technical evaluation, simulator validation testing, and
+biennial review as part of operator requalification under 10 CFR
+55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
+\oldt{formal verification of key safety properties.} \newt{exhaustive
+verification of key safety properties.}\dasinline{Does the audience know
+what formal verification is at this point? Probably, but should say
+differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
+exists that procedures cover all possible plant states, that required actions
+can be completed within available timeframes, or that transitions between
+procedure sets maintain safety invariants.
 
-Nuclear plants operate with multiple control modes: automatic control, where the
-reactor control system maintains target parameters through continuous reactivity
-adjustment; manual control, where operators directly manipulate the reactor; and
-various intermediate modes. In typical pressurized water reactor operation, the
-reactor control system automatically maintains a floating average temperature
-and compensates for power demand changes through reactivity feedback loops
-alone. Safety systems, by contrast, operate with implemented automation. Reactor
-Protection Systems trip automatically on safety signals with millisecond
-response times, and engineered safety features actuate automatically on accident
-signals without operator action required.
+\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
+correctness and completeness.} \oldt{Current procedure development relies on
+expert judgment and simulator validation. No mathematical proof exists that
+procedures cover all possible plant states, that required actions can be
+completed within available timeframes, or that transitions between procedure
+sets maintain safety invariants. Paper-based procedures cannot ensure correct
+application, and even computer-based procedure systems lack the formal
+guarantees that automated reasoning could provide.} \newt{Paper-based
+procedures cannot ensure correct application, and even computer-based
+procedure systems lack the guarantees that automated reasoning could
+provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
+sentence almost verbatim from the paragraph above. Either cut it from the
+paragraph or from the LIMITATION box.}
 
-\dasinline{After reading the next sentence, ``key safety''
-can honestly just be a semicolon.}
-\dasinline{Not sure what the challenge actually is
-as this paragraph is written. What's the point?}
-The division between automated and human-controlled functions reveals the
-fundamental challenge of hybrid control. Highly automated systems handle reactor
-protection---automatic trips on safety parameters, emergency core cooling
+Nuclear plants operate with multiple control modes: automatic control, where
+the reactor control system maintains target parameters through continuous
+reactivity adjustment; manual control, where operators directly manipulate
+the reactor; and various intermediate modes. In typical pressurized water
+reactor operation, the reactor control system automatically maintains a
+floating average temperature and compensates for power demand changes through
+reactivity feedback loops alone. Safety systems, by contrast, operate with
+implemented automation. Reactor Protection Systems trip automatically on
+safety signals with millisecond response times, and engineered safety
+features actuate automatically on accident signals without operator action
+required.
+
+\oldt{The division between automated and human-controlled functions reveals
+the fundamental challenge of hybrid control. Highly automated systems handle
+reactor protection---automatic trips on safety parameters, emergency core
+cooling actuation, containment isolation, and basic process
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
+operators, however, retain control of strategic decision-making: power level
+changes, startup/shutdown sequences, mode transitions, and procedure
+implementation.} \newt{This division between automated and human-controlled
+functions is itself the hybrid control problem. Automated systems handle
+reactor protection: trips on safety parameters, emergency core cooling
 actuation, containment isolation, and basic process
-control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
-however, retain control of strategic decision-making: power level changes,
-startup/shutdown sequences, mode transitions, and procedure 
-implementation.\splitnote{This is the key insight — the hybrid nature is 
-already there, just not formally verified.}
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
+operators retain control of everything else: power level changes,
+startup/shutdown sequences, mode transitions, and procedure
+implementation.}\dasinline{After reading the next sentence, ``key safety''
+can honestly just be a semicolon.}\dasinline{Not sure what the challenge
+actually is as this paragraph is written. What's the
+point?}\splitnote{This is the key insight — the hybrid nature is already
+there, just not formally verified.}
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Current-generation nuclear power plants employ over 3,600 active NRC-licensed
-reactor operators in the United 
-States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
-be in broader impacts about running out of ROs?
-As it is here I have no idea why this is here.} These
-operators divide into Reactor Operators (ROs), who manipulate reactor controls,
-and Senior Reactor Operators (SROs), who direct plant operations and serve as
-shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
-and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
-operator requires several years of training.
+\oldt{Current-generation nuclear power plants employ over 3,600 active
+NRC-licensed reactor operators in the United
+States~\cite{operator_statistics}. These operators divide into Reactor
+Operators (ROs), who manipulate reactor controls, and Senior Reactor
+Operators (SROs), who direct plant operations and serve as shift
+supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and
+one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
+operator requires several years of training.} \newt{Nuclear plant staffing
+requires at least two Reactor Operators (ROs) and one Senior Reactor
+Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several
+years of training and NRC licensing under 10 CFR Part
+55~\cite{10CFR55}.}\dasinline{Why is this here? Should this be in broader
+impacts about running out of ROs? As it is here I have no idea why this is
+here.}
 
-The persistent role of human error in nuclear safety incidents---despite decades
-of improvements in training and procedures---provides the most compelling
-motivation for formal automated control with mathematical safety 
-guarantees.\splitnote{Strong thesis for this subsection.}
-Operators hold legal authority under 10 CFR Part 55 to make critical 
-decisions,\dasinline{Cite.}
-including departing from normal regulations during emergencies. 
-\dasinline{Needs a connector here. Like ``But this can
-in and of itself prime plants for an accident.''
-Then continue.}The Three Mile
-Island (TMI) accident demonstrated how a combination of personnel error, design
-deficiencies, and component failures led to partial meltdown when operators
-misread confusing and contradictory readings and shut off the emergency water
-system~\cite{Kemeny1979}. The President's Commission on TMI identified a
-fundamental ambiguity: placing responsibility for safe power plant operations on
-the licensee without formal verification that operators can fulfill this
-responsibility does not guarantee safety. This tension between operational
-flexibility and safety assurance remains unresolved: the person responsible for
-reactor safety is often the root cause of 
-failures.\splitnote{``the person responsible for reactor safety is often the 
-root cause of failures'' — devastating summary. Very effective.}
+The persistent role of human error in nuclear safety incidents---despite
+decades of improvements in training and procedures---provides the most
+compelling motivation for formal automated control with mathematical safety
+guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
+legal authority under 10 CFR Part 55 to make critical
+decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
+regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
+\newt{This authority itself introduces risk. The Three Mile Island (TMI)
+accident}\dasinline{Needs a connector here. Like ``But this can in and of
+itself prime plants for an accident.'' Then continue.} demonstrated how a
+combination of personnel error, design deficiencies, and component failures
+led to partial meltdown when operators misread confusing and contradictory
+readings and shut off the emergency water system~\cite{Kemeny1979}. The
+President's Commission on TMI identified a fundamental ambiguity: placing
+responsibility for safe power plant operations on the licensee without
+formal verification that operators can fulfill this responsibility does not
+guarantee safety. This tension between operational flexibility and safety
+assurance remains unresolved: the person responsible for reactor safety is
+often the root cause of failures.\splitnote{``the person responsible for
+reactor safety is often the root cause of failures'' — devastating summary.
+Very effective.}
 
 Multiple independent analyses converge on a striking statistic: 70--80\% of
-nuclear power plant events are attributed to human error, versus approximately
-20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
-all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
-Fukushima Daiichi---has been identified as poor safety management and safety
-culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
-of 190 events at Chinese nuclear power plants from
-2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
-errors, while 92\% were associated with latent errors---organizational and
-systemic weaknesses that create conditions for 
-failure.\splitnote{Strong empirical grounding. The Chinese plant data is a 
+nuclear power plant events are attributed to human error, versus
+approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
+the root cause of all severe accidents at nuclear power plants---Three Mile
+Island, Chernobyl, and Fukushima Daiichi---has been identified as poor
+safety management and safety culture: primarily human
+factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
+Chinese nuclear power plants from
+2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
+active errors, while 92\% were associated with latent
+errors---organizational and systemic weaknesses that create conditions for
+failure.\splitnote{Strong empirical grounding. The Chinese plant data is a
 nice addition — shows this isn't just a Western regulatory perspective.}
 
 
-\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
-that cannot be overcome through training alone.} The persistent human
-error contribution despite four decades of improvements demonstrates that these
-limitations are fundamental rather than a remediable part of human-driven 
-control.\splitnote{Well-stated. The ``four decades'' point drives it home.}
+\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
+limits that cannot be overcome through training alone.} The persistent human
+error contribution despite four decades of improvements demonstrates that
+these limitations are fundamental rather than a remediable part of
+human-driven control.\splitnote{Well-stated. The ``four decades'' point
+drives it home.}
 
 \subsection{Formal Methods}
 \subsubsection{HARDENS}
 
 The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
-project represents the most advanced application of formal methods to nuclear
-reactor control systems to date~\cite{Kiniry2024}.
+project represents the most advanced application of formal methods to
+nuclear reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
-rooms rely on analog technologies from the 1950s--60s.\dasinline{Source?}
-This technology is
-obsolete compared to modern control systems and incurs significant risk and
-cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
-Model-Based Systems Engineering and formal methods could design, verify, and
-implement a complex protection system meeting regulatory criteria at a fraction
-of typical cost. The project delivered a Reactor Trip System (RTS)
-implementation with full traceability from NRC Request for Proposals and IEEE
-standards through formal architecture specifications to verified 
-software.\dasinline{Wordsmith this to remove the RFP and
-IEEE standards language. Should just say
-requirements.}
+HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear
+control rooms rely on analog technologies from the
+1950s--60s.\dasinline{Source?} This technology is obsolete compared to
+modern control systems and incurs significant risk and cost. The NRC
+contracted Galois, a formal methods firm, to demonstrate that Model-Based
+Systems Engineering and formal methods could design, verify, and implement a
+complex protection system meeting regulatory criteria at a fraction of
+typical cost. The project delivered a Reactor Trip System (RTS)
+implementation with full traceability from \oldt{NRC Request for Proposals
+and IEEE standards through formal architecture specifications to verified
+software.} \newt{regulatory requirements through formal architecture
+specifications to verified software.}\dasinline{Wordsmith this to remove the
+RFP and IEEE standards language. Should just say requirements.}
 
-HARDENS employed formal methods tools and techniques across the verification
-hierarchy.\dasinline{Zero discussion about what the
-verification hierarchy is. What is a specification
-or a requirement to someone who hasn't heard of
-one before?} High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
-Requirements Elicitation Tool) to capture stakeholder requirements, domain
-engineering, certification requirements, and safety requirements. Requirements
-were analyzed for consistency, completeness, and realizability using SAT and SMT
-solvers. Executable formal models used Cryptol to create a behavioral model of
-the entire RTS, including all subsystems, components, and limited digital twin
+\oldt{HARDENS employed formal methods tools and techniques across the
+verification hierarchy.} \newt{HARDENS employed formal methods tools at
+every level of system development, from high-level requirements through
+executable models to generated code.}\dasinline{Zero discussion about what
+the verification hierarchy is. What is a specification or a requirement to
+someone who hasn't heard of one before?} High-level specifications used
+Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
+capture stakeholder requirements, domain engineering, certification
+requirements, and safety requirements. Requirements were analyzed for
+consistency, completeness, and realizability using SAT and SMT solvers.
+Executable formal models used Cryptol to create a behavioral model of the
+entire RTS, including all subsystems, components, and limited digital twin
 models of sensors, actuators, and compute infrastructure. Automatic code
 synthesis generated verifiable C implementations and SystemVerilog hardware
-implementations directly from Cryptol models---eliminating the traditional gap
-between specification and implementation where errors commonly 
+implementations directly from Cryptol models---eliminating the traditional
+gap between specification and implementation where errors commonly
 arise.\splitnote{Good technical depth on HARDENS toolchain.}
 
-Despite its accomplishments, HARDENS has a fundamental limitation directly
-relevant to hybrid control synthesis: the project addressed only discrete
-digital control logic without modeling or verifying continuous reactor 
-dynamics.\dasinline{Edit these to more clearly separate
-the context from the limit. The limitation should
-be in the limitation.}
-The Reactor Trip System specification and verification covered discrete state
-transitions (trip/no-trip decisions), digital sensor input processing through
-discrete logic, and discrete actuation outputs (reactor trip commands). The
-project did not address continuous dynamics of nuclear reactor physics. Real
-reactor safety depends on the interaction between continuous
-processes---temperature, pressure, neutron flux---evolving in response to
-discrete control decisions. HARDENS verified the discrete controller in
-isolation but not the closed-loop hybrid system 
-behavior.\splitnote{Clear articulation of the gap your work fills.}
+\oldt{Despite its accomplishments, HARDENS has a fundamental limitation
+directly relevant to hybrid control synthesis: the project addressed only
+discrete digital control logic without modeling or verifying continuous
+reactor dynamics. The Reactor Trip System specification and verification
+covered discrete state transitions (trip/no-trip decisions), digital sensor
+input processing through discrete logic, and discrete actuation outputs
+(reactor trip commands). The project did not address continuous dynamics of
+nuclear reactor physics. Real reactor safety depends on the interaction
+between continuous processes---temperature, pressure, neutron flux---evolving
+in response to discrete control decisions. HARDENS verified the discrete
+controller in isolation but not the closed-loop hybrid system behavior.}
+\newt{Despite these accomplishments, HARDENS addressed only discrete digital
+control logic. The Reactor Trip System verification covered discrete state
+transitions, digital sensor processing, and discrete actuation outputs. It
+did not model or verify continuous reactor dynamics. Real reactor safety
+depends on the interaction between continuous processes---temperature,
+pressure, neutron flux---evolving in response to discrete control decisions.
+HARDENS verified the discrete controller in isolation but not the
+closed-loop hybrid system behavior.}\dasinline{Edit these to more clearly
+separate the context from the limit. The limitation should be in the
+limitation.}\splitnote{Clear articulation of the gap your work fills.}
 
-\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
-continuous dynamics or hybrid system verification.} Verifying discrete control
-logic alone provides no guarantee that the closed-loop system exhibits desired
-continuous behavior such as stability, convergence to setpoints, or maintained
-safety margins.
+\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
+without continuous dynamics or hybrid system verification.} Verifying
+discrete control logic alone provides no guarantee that the closed-loop
+system exhibits desired continuous behavior such as stability, convergence to
+setpoints, or maintained safety margins.
 
 HARDENS produced a demonstrator system at Technology Readiness Level 2--3
-(analytical proof of concept with laboratory breadboard validation) rather than
-a deployment-ready system validated through extended operational testing. The
-NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
-considered in development, not a finalized product, and that ``The demonstration
-of its technical soundness was to be at a level consistent with satisfaction of
-the current regulatory criteria, although with no explicit demonstration of how
-regulatory requirements are 
-met.''\dasinline{Check this quote. Absolutely damning
-for HARDENS if true and hilarious Galois said
-this.} The project did not include deployment in
-actual nuclear facilities, testing with real reactor systems under operational
-conditions, side-by-side validation with operational analog RTS systems,
-systematic failure mode testing (radiation effects, electromagnetic
-interference, temperature extremes), NRC licensing review, or human factors
-validation with licensed operators in realistic control room scenarios.
+(analytical proof of concept with laboratory breadboard validation) rather
+than a deployment-ready system validated through extended operational
+testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all
+material is considered in development, not a finalized product, and that
+``The demonstration of its technical soundness was to be at a level
+consistent with satisfaction of the current regulatory criteria, although
+with no explicit demonstration of how regulatory requirements are
+met.''\dasinline{Check this quote. Absolutely damning for HARDENS if true
+and hilarious Galois said this.} The project did not include deployment in
+actual nuclear facilities, testing with real reactor systems under
+operational conditions, side-by-side validation with operational analog RTS
+systems, systematic failure mode testing, NRC licensing review, or human
+factors validation with licensed operators in realistic control room
+scenarios.
 
 \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
-validation.}\dasinline{Same as before. Separate limit
-from context better.} While formal verification provides mathematical correctness
-guarantees for the implemented discrete logic, the gap between formal
-verification and actual system deployment involves myriad practical
-considerations: integration with legacy systems, long-term reliability
-under harsh environments, human-system interaction in realistic
-operational contexts, and regulatory acceptance of formal methods as
-primary assurance evidence.
+validation.} \oldt{While formal verification provides mathematical
+correctness guarantees for the implemented discrete logic, the gap between
+formal verification and actual system deployment involves myriad practical
+considerations: integration with legacy systems, long-term reliability under
+harsh environments, human-system interaction in realistic operational
+contexts, and regulatory acceptance of formal methods as primary assurance
+evidence.} \newt{The gap between formal verification and actual system
+deployment remains wide: integration with legacy systems, long-term
+reliability under harsh environments, human-system interaction, and
+regulatory acceptance of formal methods as primary assurance
+evidence.}\dasinline{Same as before. Separate limit from context better.}
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
-There has been additional work to do verification of hybrid systems by extending
-the temporal logics 
-directly.\dasinline{Need to introduce temporal logic
-and FRET here first.} The result has been the field of differential
-dynamic logic (dL). dL introduces two additional operators
-into temporal logic: the box operator and the diamond operator. The box operator
-\([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
-\(\alpha\) always remains within that region. In this way, it is a safety
-ivariant being enforced for the system.\splitfix{Typo: ``ivariant'' should be 
-``invariant''} The second operator, the diamond
-operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
-one trajectory of \(\alpha\) that enters that region. This is a declaration of a
-liveness property. 
+\oldt{There has been additional work to do verification of hybrid systems by
+extending the temporal logics directly.} \newt{A separate line of work
+extends temporal logics to verify hybrid systems
+directly.}\dasinline{Need to introduce temporal logic and FRET here first.}
+The result has been the field of differential dynamic logic (dL). dL
+introduces two additional operators into temporal logic: the box operator and
+the diamond operator. The box operator \([\alpha]\phi\) states that for some
+region \(\phi\), the hybrid system \(\alpha\) always remains within that
+region. In this way, it is a safety \oldt{ivariant} \newt{invariant} being
+enforced for the system.\splitfix{Typo: ``ivariant'' should be
+``invariant''} The second operator, the diamond operator
+\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
+trajectory of \(\alpha\) that enters that region. This is a declaration of a
+liveness property.
 
 %source: https://symbolaris.com/logic/dL.html
 
-While dL allows for the specification of these liveness and safety properties,
-actually proving them for a given hybrid system is quite difficult. Automated
-proof assistants such as KeYmaera X exist to help develop proofs of systems
-using dL, but so far have been insufficient for reasonably complex hybrid
-systems. The main issue behind creating system proofs using dL is state space
-explosion and non-terminating 
-solutions.\splitsuggest{Consider adding a concrete example here — ``For 
-instance, a system with N modes and M continuous state variables...'' to give 
-readers a sense of the scaling problem.}
+While dL allows for the specification of these liveness and safety
+properties, actually proving them for a given hybrid system is quite
+difficult. Automated proof assistants such as KeYmaera X exist to help
+develop proofs of systems using dL, but so far have been insufficient for
+reasonably complex hybrid systems. The main issue behind creating system
+proofs using dL is state space explosion and non-terminating solutions.
 %Source: that one satellite tracking paper that has the problem with the
 %gyroscopes overloding and needing to dump speed all the time
-Approaches have been made to alleviate
-these issues for nuclear power contexts using contract and decomposition based
-methods, but are far from a complete methodology to design systems 
-with.\splitpolish{``but are far from a complete methodology to design systems 
-with'' — awkward ending preposition. Try: ``but remain far from a complete 
-design methodology'' or ``but do not yet constitute a complete design 
-methodology.''}
-%source: Manyu's thesis. 
+Approaches have been made to alleviate these issues for nuclear power
+contexts using contract and decomposition based methods, \oldt{but are far
+from a complete methodology to design systems with.} \newt{but do not yet
+constitute a complete design methodology.}\splitpolish{``but are far from a
+complete methodology to design systems with'' — awkward ending preposition.}
+%source: Manyu's thesis.
 Instead, these approaches have been used on systems that have been designed a
-priori, and require expert knowledge to create the system proofs. 
+priori, and require expert knowledge to create the system proofs.
 
 %Maybe a limitation here? Something about dL doesn't scale or help in design
-%very much, so the limitation is that logic based hybrid system approaches have
-%not been used in the DESIGN of autonomous controllers, only in the analysis of
-%systems that already exist.
-\splitinline{Your comment here is spot-on. You should add a LIMITATION box: 
-\textit{Differential dynamic logic has been used for post-hoc analysis of 
-existing systems, not for the constructive design of autonomous controllers.} 
-This is exactly the gap you're filling — you're doing synthesis, not just 
-verification.}
+%very much, so the limitation is that logic based hybrid system approaches
+%have not been used in the DESIGN of autonomous controllers, only in the
+%analysis of systems that already exist.
+
+\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
+post-hoc analysis of existing systems, not for the constructive design of
+autonomous controllers.} Current dL-based approaches verify systems that
+have already been designed, requiring expert knowledge to construct proofs.
+They have not been applied to the synthesis of new controllers from
+operational requirements.\splitinline{Your comment here is spot-on. You
+should add a LIMITATION box: \textit{Differential dynamic logic has been
+used for post-hoc analysis of existing systems, not for the constructive
+design of autonomous controllers.} This is exactly the gap you're filling —
+you're doing synthesis, not just verification.}