# Preliminary Example Presentation — Assertion-Evidence Outline **Format:** Assertion-evidence (Alley). Each slide: one declarative sentence at the top, one piece of visual evidence below. No bullet soup. **Duration:** 20 minutes. ~11 content slides + title + Q&A. ~1.5–2 min/slide, heavier on slides 1, 9, 10. Buffer ~1 min. **Audience:** OT-informed cybersecurity experts. Mostly CS, some control-theory familiarity, very little reactor-physics background. Can assume fluency with: LTL, automata, model-checking, reachability (as a concept), SMT/SAT. Must explain: PKE, reactivity, precursors, hybrid systems. **Running thread:** procedures → FRET → LTL/AIGER → DRC → continuous gotcha → plant model → reach with stiffness wall → prompt-jump fix (with validity-as-an- invariant) → two sound nonlinear results → seam. **Design principles:** - **Plots over bullets.** Every result slide anchors on one figure. - **Physical intuition before math.** Reactor basics in passing, not as a tutorial. - **Honest limitations on each result slide.** Audience are cyber folks — they respect limits more than triumphs. - **CS vocabulary by default, engineering terms defined inline.** - **End with the seam**, not with a victory lap. The thesis question is "how do discrete proofs and continuous proofs compose?" not "we verified everything." --- ## Slide 1 — Title + hook + scopes of control (2-frame animation) **Assertion (frame 1):** Nuclear reactor operation is dominated by humans following procedures, and the procedures themselves have no formal verification. **Evidence (frame 1):** Full-bleed photograph of a control room — analog gauges, paper procedures on the desk, two operators. **Speak (frame 1):** Self + advisor + NRC fellowship. The hook: most plants are run by humans following paper procedures. We've been engineering humans *out* of the loop for forty years by making the procedures more and more prescriptive — but the procedures themselves are written natural language. We rely on humans to follow them faithfully and on tradition to keep them correct. (Soften: "running a nuclear reactor is well-understood" — the *procedures* are a knowledge-engineering artifact built over decades.) **Assertion (frame 2):** Plant control decomposes into three scopes — strategic, operational, tactical — and formal methods most naturally land on the *operational* scope. **Evidence (frame 2):** Photo slides left to make room for a 3-tier pyramid on the right: ``` ┌──────────────────┐ │ STRATEGIC │ start it up / shut it down (hours-days) └──────────────────┘ ┌──────────────────────┐ │ OPERATIONAL │ heat up / run / scram (minutes-hours) └──────────────────────┘ ┌──────────────────────────┐ │ TACTICAL │ rod motion, valve actuation (seconds) └──────────────────────────┘ ``` **Speak (frame 2):** Strategic = mission-level decisions, operator authority. Tactical = millisecond-scale rod and valve commands, classical control. The **operational** middle is where the procedures live — "if cold and ready, heat up; if at temperature and critical, switch to power operation; if any trip condition, scram." This middle is where formal methods can do their best work because the dynamics are slow enough to verify and the logic is discrete enough to specify. The thesis lives here. **Reference:** thesis §2, ¶1-4. Cites Kemeny1979, Hogberg_2013, Kiniry2024. **Figures to make:** control-room photo (license-clean source TBD); pyramid diagram (Tikz, simple). --- ## Slide 2 — FRET requirements: capture the procedure, find the seam **Assertion:** FRET turns natural-language operational procedures into LTL, and reveals the seam where a discrete predicate lands on a continuous state. **Evidence:** A two-row figure. Top row: a FRET requirement card. > **PWR-2001:** Upon `control_mode = q_heatup ∧ t_avg_in_range ∧ p_above_crit ∧ inv1_holds`, DRC shall at the next timepoint satisfy `control_mode = q_operation`. Bottom row: the corresponding LTL, with one of the boolean atoms (`t_avg_in_range`) circled in red. Side annotation: > `t_avg_in_range` ≡ |T_c − T_c0| ≤ 2.78 °C > *(this is a half-space on a continuous state)* **Speak:** FRET writes requirements like "if A then next B" in a restricted natural-language template. Spot's compiler (FRET → LTL) checks that the requirement set is *realizable* — there exists a discrete controller that satisfies all requirements. **Here's the part that matters for hybrid systems:** some of these boolean atoms aren't really boolean. `t_avg_in_range` is a halfspace on a continuous state vector. The discrete controller treats it as true-or-false; the continuous plant has to actually *make it true* under whatever dynamics apply. **That gap — between the discrete requirement and the continuous truth-maker — is the seam.** The whole rest of the talk is about discharging that seam. **Reference:** `fret-pipeline/pwr_hybrid_3.json`, `reachability/predicates.json`. **Figures to make:** FRET-card visual + LTL panel. --- ## Slide 3 — From LTL to a synthesized discrete controller **Assertion:** Reactive synthesis (Spot/ltlsynt) compiles the LTL into an AIGER circuit — the minimal correct discrete controller — automatically. **Evidence:** Pipeline figure. Three boxes left-to-right: ``` [ FRET requirements ] → [ LTL formula ] → [ AIGER circuit ] (realizability check) (ltlsynt synthesis) (.aag file) ``` Below the third box: a thumbnail of the synthesized DRC state diagram (`fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png`). **Speak:** Two distinct things are happening. **FRET's realizability check** says "your requirements are mutually consistent and a controller exists." **Spot/ltlsynt's reactive synthesis** actually *builds* that controller — it solves a parity game on the LTL formula and emits an AIGER circuit, the minimal-state controller satisfying the spec. We then extract the state diagram from the AIGER. This is well-established machinery in the formal-methods world; our contribution is *applying it to reactor operating procedures*, which is a formal-methods-free domain historically. **Reference:** `fret-pipeline/scripts/fret_to_synth.py`, `circuits/PWR_HYBRID_3_DRC.aag`. --- ## Slide 4 — The synthesized DRC for PWR_HYBRID_3 **Assertion:** The discrete controller for our running example has four modes and seven transitions, all driven by predicates on the continuous state. **Evidence:** Full-slide DRC state diagram from `fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png`. Annotated with transition guards, e.g. `t_avg_in_range ∧ p_above_crit ∧ inv1_holds` on the heatup→operation arrow. **Speak:** Cold shutdown, heatup, power operation, scram. Every transition is gated by a conjunction of atomic predicates. Each predicate is a halfspace on the 10-dimensional plant state. So the discrete controller's correctness *as a hybrid system* depends entirely on whether the continuous plant trajectory makes the right predicates true at the right moments. Which brings us to the gotcha. **Reference:** `fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png`. --- ## Slide 5 — The continuous gotcha **Assertion:** A correct discrete controller does not imply a correct hybrid system; the continuous-side predicates have to be discharged separately. **Evidence:** A simple 2-panel cartoon. Left: DRC state diagram with one transition arrow highlighted. Right: a 2D phase portrait sketch with the trajectory drifting *outside* the predicate region — controller fires the transition based on logic, but the plant isn't actually where the logic thinks it is. **Speak:** The DRC is correct as a discrete object — it satisfies all the LTL requirements *given* its predicate inputs. But predicates like `t_avg_in_range` are continuous-state halfspaces. If the plant's actual trajectory leaves that halfspace while the controller still believes it's inside, the discrete proof is meaningless. We need a *continuous-side proof* that the plant actually inhabits the right halfspaces at the right times. That proof is per-mode and the methodology contribution of the chapter. --- ## Slide 6 — The plant model: 10-state PKE + thermal-hydraulics **Assertion:** A 10-state point-kinetic + lumped thermal-hydraulics PWR model is the continuous-side surrogate — faithful enough to verify, stiff enough to give us trouble. **Evidence:** State-vector coupling diagram showing the chain `u (rods) → ρ → n → P → T_f → T_c → T_cold → ρ_feedback`, with `Q_sg` as a bounded disturbance on `T_cold`. ``` state x = [ n C₁..C₆ T_f T_c T_cold ] └──prompt──┘ └─────thermal─────┘ (Λ ≈ 10⁻⁴ s) (τ ≈ 10–100 s) ↑ stiffness ratio ≈ 10⁵ ``` **Speak:** Point-kinetic equations for neutron population and six delayed-neutron precursor groups. Three thermal nodes — fuel, average coolant, cold-leg. One control input (rod-induced reactivity). One bounded disturbance (steam-generator heat removal). **Stiffness ratio of 10⁵ between prompt-neutron and thermal timescales.** Flag this now — it's about to be the cliff. **Reference:** `code/src/pke_th_rhs.jl`, journal entry 2026-04-17. **Figures to make:** state-vector coupling diagram (Tikz). --- ## Slide 7 — Per-mode reach-avoid obligations **Assertion:** Discrete-to-continuous correctness reduces to one reach-avoid obligation per mode — equilibrium modes prove forever-invariance, transition modes prove bounded-time reach-avoid. **Evidence:** Compact taxonomy: | Mode | Kind | Obligation | |---|---|---| | shutdown / operation | equilibrium | stay in safe set forever | | heatup / scram | transition | from X_entry, reach X_exit in [T_min, T_max], stay safe | Below the table: a tiny phase-portrait pictogram for each kind — bowl (equilibrium) vs corridor (transition). **Speak:** This is the structural insight. If every mode's obligation is discharged, the hybrid system is correct by composition — the discrete controller's transitions fire correctly because the continuous plant *actually arrives* at each `X_exit` predicate by the time the transition guard is checked. Two flavors of obligation. Two flavors of proof. **Reference:** `reachability/WALKTHROUGH.md` §1. --- ## Slide 8 — First reach attempt: stiffness wall **Assertion:** Naive nonlinear reach (TMJets) caps out at ~10 seconds of horizon on the full 10-state model — orders of magnitude short of what the obligations need. **Evidence:** A two-panel figure. Left: a graph of horizon achieved vs wall-clock time, asymptoting at ~10 s of plant time. Right: a one-line caption — "T_max(heatup) = 5 hr; T_max(scram) = 60 s. We're 1800× short on heatup and 6× short on scram." **Speak:** TMJets is a Taylor-model integrator — produces *sound* over-approximations of the nonlinear reach set. Beautiful tool. But its step size is bounded by the *fastest* dynamics in the system, which here is the prompt-neutron timescale `Λ ≈ 10⁻⁴ s`. Even on a bounded reach horizon, you blow your step budget propagating Taylor models that nobody cares about, because nothing safety-relevant happens on that timescale. **The stiffness ratio kills us.** We need to remove the fast modes without losing soundness. **Reference:** `code/scripts/reach/reach_heatup_nonlinear.jl`. --- ## Slide 9 — Prompt-jump reduction with validity-as-an-invariant **Assertion:** Singular-perturbation reduction eliminates the prompt neutronics, gives us 30× more reach horizon — and, critically, the reduction's validity condition becomes part of the safety obligation itself, not a separate hand-wave. **Evidence:** Two stacked panels. Top: the algebraic substitution. $$\frac{dn}{dt} = 0 \implies n = \frac{\Lambda \sum_i \lambda_i C_i}{\beta - \rho(x)}$$ State drops from 10 to 9. Stiffness gone. Reach steps now bounded by thermal timescale, not prompt timescale. Bottom: the validity condition + Tikhonov bound. - Validity: `β − ρ(x) > δ > 0` over the reach set — this is a half-space in the same vocabulary as every other safety predicate. - Error: `|x(t) − x_PJ(t)| ≤ C·Λ = O(10⁻⁴)` (Tikhonov). **Speak:** The trick that makes this thesis-shaped: we don't *assume* the prompt-jump reduction is valid — we **prove** it as part of the same reach obligation. The halfspace `prompt_critical_margin_holds` is in the per-mode invariant set right alongside the safety halfspaces. If reach discharges the invariant, it discharges *both* safety and the approximation's soundness. No separate validity argument. This is the formal-methods-shaped move I want the audience to take home. **Reference:** `code/src/pke_th_rhs_pj.jl`, journal entry 2026-04-21 "Tikhonov bound", `reachability/predicates.json::prompt_critical_margin_*`. --- ## Slide 10 — Two sound nonlinear reach proofs **Assertion:** With prompt-jump, both transition modes — heatup and scram — discharge their full safety invariants over their relevant horizons. **Evidence:** Side-by-side, two panels. Left panel — **heatup**: tube plot from `docs/figures/reach_heatup_pj_tubes.png`. Caption: "300 s, all 6 `inv1_holds` halfspaces discharged, T_c stable at [281.05, 291.0] °C." Right panel — **scram**: shutdown-margin discharge from `results/reach_scram_pj_fat.mat`. A bar chart of |ρ| vs the 1% Δk/k floor at T = 10, 30, 60 s. Caption: "Fat entry polytope (union of all mode envelopes). |ρ| ≈ 5%. **5× the requirement at 60 s.**" **Speak:** **Heatup**: 12,932 reach-sets, 200 s wall, tube stable — `T_c` envelope identical at 60 s and 300 s, meaning the controller holds the state inside the tube indefinitely. **Scram**: from the fat entry polytope (any state the plant could be in across all modes plus LOCA), the shutdown-margin halfspace discharges at 10, 30, *and* 60 s with five times the NRC tech-spec margin. Both are sound for the prompt-jump-reduced plant; both inherit the O(Λ) Tikhonov error to the full plant. **Two transition modes formally verified end-to-end.** This is the headline result. **Limitations box:** 300 s of a 5-hour `T_max` on heatup. Step budget is the wall; entry refinement is the path to hours. **Evidence path:** `code/scripts/reach/reach_heatup_pj.jl`, `code/scripts/reach/reach_scram_pj_fat.jl`, `docs/figures/reach_heatup_pj_tubes.png`, `results/reach_scram_pj_fat.mat`. --- ## Slide 11 — Composition + impact + the open seam **Assertion:** Two transition modes verified, two equilibrium modes are the next step — the composition story holds, the open question is well-defined. **Evidence:** Two-column layout. Left column — **what's proven** (with a green check): | Mode | Status | |---|---| | Heatup | Sound nonlinear reach, 300 s, all 6 safety halfspaces | | Scram | Sound nonlinear reach, 60 s, shutdown margin, 5× tech-spec | | FRET → AIGER | Sound discrete controller, realizability checked | | PJ validity | Discharged inside the same reach obligation | Right column — **what's next** (amber): | Open | Path | |---|---| | Operation mode forever-invariance | Polynomial barrier certificate (SOS) on PJ dynamics | | Hot-standby forever-invariance | Same machinery, different equilibrium | | Full 5-hr heatup horizon | Entry refinement (Blanchini-style) | | Hardware integration | Ovation DCS, scheduled | **Speak:** Where this lands. Two transition modes, formally verified end-to-end — discrete controller from FRET, continuous trajectory bounded by sound nonlinear reach, validity of the reduction proven inside the same obligation. **The open piece is stability proofs for the equilibrium modes — operation and hot-standby.** We've started on barrier certificates to discharge those, and the machinery works on a 2D linearization, but the sound treatment on the full nonlinear plant is the next thrust. That's the work for the next several months. **The composition framework holds; we're filling in cells in the matrix.** **Cyber angle close:** Formal verification of operational procedures is defense-in-depth for OT. Even if an attacker bypasses the comms layer and injects commands, a verified DRC plus a discharged reach-avoid envelope **constrains what the physical plant can be made to do.** That's an assurance axis comms-security alone can't reach. --- ## Slide 12 — Q&A / acknowledgements (backup) **Assertion:** (none — backup slide) **Evidence:** Acknowledgements. Advisor (Cole), committee, NRC fellowship. Repo (gitea), journal PDF, thesis in progress. **Anticipated questions:** - "Why not Stateflow/Simulink?" → tool-integration story; HARDENS used Cryptol for the same reason. - "How does this interact with ML components?" → out of scope; the pitch is *no ML in the safety-critical loop*. - "What's the threat model?" → tie back to OT audience: formal methods guarantee the controller's logic and the physical plant's behavior; they do not protect comms or implementation. Defense in depth. - "Why not just do nonlinear-SOS directly?" → the thrust starts there in the next phase; the linearized 2D version was the proof-of-concept. --- ## Presentation construction notes ### Slide-count vs. time budget 11 content slides + title + Q&A. Average 1.6 min/slide. Allocation: | Slide | Min | Reason | |---|---|---| | 1 (anim) | 2.5 | Hook needs riff room | | 2 (FRET seam) | 2.0 | Audience unfamiliar; this is the central insight | | 3 | 1.5 | Pipeline diagram | | 4 | 1.5 | DRC walkthrough | | 5 | 1.0 | Transition slide, short | | 6 | 1.5 | Plant + stiffness flag | | 7 | 1.0 | Taxonomy, short | | 8 | 1.5 | Wall problem | | 9 | 2.0 | Methodology contribution; slowest | | 10 | 2.0 | Headline result | | 11 | 1.5 | Closing seam | | **Total** | **18.0** | + 2 min buffer | ### What to build in Beamer - Assertion-evidence template — one declarative sentence at top, centered figure below, optional 2-line speaker note in footer. - Color coding: green = sound/proven, amber = approximate/open, red = limitation, blue = discrete-layer, purple = continuous-layer. - 2-frame animation on slide 1 (overlay specs in Beamer). - Inset boxes on result slides for limitations (slide 10). ### Figures that need to be created or dressed up | Slide | Figure | Source / status | |---|---|---| | 1 | Control-room photo | License-clean source TBD | | 1 | Strategic/operational/tactical pyramid | Tikz, fresh | | 2 | FRET-card + LTL panel | Inkscape, fresh | | 3 | FRET → LTL → AIGER pipeline | Tikz, fresh | | 4 | DRC state diagram | `fret-pipeline/diagrams/PWR_HYBRID_3_DRC_states.png`, dress up | | 5 | DRC + drifted-trajectory cartoon | Inkscape, fresh | | 6 | State-vector coupling diagram | Tikz, fresh | | 7 | Equilibrium/transition pictograms | Tikz, simple | | 8 | Horizon-vs-walltime stiffness graph | Matplotlib, fresh | | 9 | PJ algebraic substitution + Tikhonov | LaTeX math + label | | 10 | Heatup tubes | `docs/figures/reach_heatup_pj_tubes.png`, dress up | | 10 | Scram shutdown-margin bars | Matplotlib, fresh, from `reach_scram_pj_fat.mat` | | 11 | Two-column matrix | Beamer table | ### Cybersecurity angle to emphasize (one sentence each, distributed across slides) - Slide 1: procedures are the OT-side analog of code; both deserve formal verification. - Slide 2: discrete-only verification (HARDENS) leaves the seam unaddressed. - Slide 11 close: verified physical-plant envelope is an assurance axis comms security alone cannot reach. ### Things to NOT do - Don't get lost in reactor-physics detail. One sentence per physical concept; keep the audience moving. - Don't show code unless code structure is the point. Code screenshots are weak evidence. - Don't oversell. Honest limitations build trust with skeptical audiences. - Don't use more than 2 bullet points on any slide. Alley rules. - **Don't try to fit SOS barriers as their own slide.** They live in slide 11 as one closing line about what's next. Cutting them out of the talk was a deliberate choice — say it once, move on. ### Timing checkpoints - Slide 4 (DRC) by minute 6. - Slide 7 (taxonomy) by minute 9. - Slide 9 (PJ) by minute 13. - Slide 10 (results) by minute 16. - Slide 11 (close) by minute 19. ### Cuts made vs. April-21 outline (for reference) - Slide 7 "Operation reach (the win)" — cut. Linear reach is a gut-check, not a headline. Demoted to one bullet on slide 11. - Slide 8 "Quadratic Lyapunov fails" — cut. Side-quest in this arc. - Slide 11 "Degree-4 SOS barrier" — cut as standalone slide. Folded into slide 11 "next steps" as one line. - Slide 6 mode-taxonomy table — folded into slide 7 informally; modes appear as concrete examples (heatup, scram) when verified, not as upfront enumeration. - Lyapunov bar-chart, per-halfspace margin table, tools-comparison diagram — all cut for time. - Added: scopes-of-control framing on slide 1. - Added: continuous-gotcha transition (slide 5) explicitly calling out the seam. - Added: scram reach as headline result on slide 10 (was a follow-up bullet on April-21 limitations slide).