Prac Safety Case as a Governed Process — VSL Sketch
Helios-style four-layer specification of the H₂O₂ bench prac as a chemical reactor
Year 10 Chemistry · Reactivity Rocket Project · Engineering Reasoning · Simulation companion
A Helios-style specification of the KMnO₄ + H₂O₂ Year 10 prac, treating the bench setup as an instance of a chemical reactor and applying the four-layer assurance pattern. This is illustrative — the formal grammar is approximate and intended to make the engineering reasoning concrete rather than to compile.
1 Conservation laws — invariants
These hold at every timestep of the physical process and at every state transition in the specification.
invariant mass_balance:
∀ t. Σ_species mass(species, t) = mass_total_initial
invariant energy_balance:
∀ t. ΔU_internal(t) + Q_lost(t) + W_steam(t)
= Σ_reactions r(t) · ΔH_reaction · dt
invariant species_balance_h2o2:
∀ t. n_H2O2(t) = n_H2O2(0) - ∫₀ᵗ r(τ) · V dτ
where r(τ) = k(T(τ)) · [KMnO4](τ) · [H2O2](τ)
· A · exp(-Ea / (R · T(τ)))
invariant stoichiometry_o2:
∀ t. n_O2_produced(t) = 0.5 · (n_H2O2(0) - n_H2O2(t))2 State envelope — guard predicates
The reactor is only permitted to operate inside these bounds. Any actuator that would push state outside the envelope is denied.
predicate safe_temperature:
T_peak(reactor, t) < T_critical - ΔT_spread_max
- ΔT_measurement
- ΔT_uncertainty
where T_critical = 343.15 K // 70 °C, autocatalytic onset
ΔT_spread_max = 15.0 K // unstirred test tube bound
ΔT_measurement = 3.0 K // probe placement + reading
ΔT_uncertainty = 7.0 K // batch and concentration variation
predicate safe_concentration:
[H2O2]_initial ≤ 0.06 (w/w) // 6% maximum
∧ [KMnO4]_initial ≤ 0.01 mol/L
predicate adequate_venting:
V_vessel_headspace ≥ 5 · V_O2_stoichiometric(T_max)
predicate stirring_active:
ω_stir(t) ≥ ω_min ∀ t ∈ [t_initiation, t_completion]
where ω_min sufficient to maintain ΔT_spread < ΔT_spread_max
predicate operator_present:
supervisor_in_room(t) = true ∀ t ∈ [t_setup, t_disposal]3 Action legs — what may happen
In Helios terms, every state transition is an ActionLeg with explicit pre- and post-conditions. The full set for this prac is small:
action_leg add_kmno4:
precondition:
state = reagents_prepared
∧ safe_temperature ∧ safe_concentration
∧ adequate_venting ∧ stirring_active
∧ operator_present
effect:
[KMnO4](t⁺) = [KMnO4]_target
state → reacting
postcondition:
safe_temperature still holds
action_leg sample_temperature:
precondition:
state ∈ {reacting, completing}
effect:
record(T_reading, t)
if T_reading > 45 °C then emit warning_event
action_leg sample_volume:
precondition:
state ∈ {reacting, completing}
effect:
record(V_O2_reading, t)
action_leg emergency_quench:
precondition:
warning_event_active ∨ T_reading > 50 °C
effect:
transfer_to_cold_bath
state → quenched
postcondition:
T_bulk → T_ambient within Δt_quench
action_leg complete:
precondition:
dV_O2/dt < 0.3 mL/s for 30 s
effect:
state → completed
disposal_required = trueNotice that emergency_quench is itself in the action set with formal pre- and post-conditions. Safety actions are first-class, not afterthoughts.
4 Forbidden transitions — explicit non-actions
Equally important: the actions that must never occur, with their refusal conditions.
forbidden cap_vessel:
∀ t ∈ [t_setup, t_completion]. ¬ vessel_sealed(t)
forbidden increase_concentration_during_run:
∀ t > t_initiation. d[H2O2]/dt ≤ 0 ∧ d[KMnO4]/dt ≤ 0
forbidden remove_from_bath_while_hot:
¬ (T_bulk > T_ambient + 5 K ∧ remove_from_bath_action)
forbidden add_organic_material:
∀ t. organic_introduction(t) = ∅5 Lean proof obligations
The conservation invariants compose into theorems the prac is designed to satisfy. These are the safety theorems that the entire engineering controls assembly is meant to make true:
theorem safety_temperature_bound :
∀ (s : ReactorState),
s.initial_concentration ≤ 0.06 →
s.stirring = active →
s.heat_loss_coefficient ≥ h_min →
∀ t, s.T_peak(t) < T_critical
theorem completion_terminates :
∀ (s : ReactorState),
s.initial_concentration ≤ 0.06 →
∃ t_final, t_final < t_max ∧
s.completion_predicate(t_final) = true
theorem quench_is_effective :
∀ (s : ReactorState),
s.T_peak < T_critical →
quench_action(s).T_bulk(t + Δt_quench) ≤ T_ambient + 5 KThe first theorem says: if you start within the concentration envelope and maintain stirring and heat loss, peak temperature never reaches the autocatalytic threshold. This is what makes the prac safe by construction rather than by hope.
6 Rust test layer
The simulation models you have are the executable manifestation of this specification. The 0-D model is an instance of the energy-balance invariant; the 2D model is an instance of the spread-bound predicate. Property-based tests in Rust would generate random valid input states (concentrations, volumes, temperatures, stirring intensities within envelope) and assert:
proptest! {
#[test]
fn safe_envelope_implies_safe_peak(
h2o2_pct in 1.0..6.0_f64,
kmno4_mM in 1.0..10.0_f64,
vol_mL in 10.0..200.0_f64,
T_start_C in 5.0..30.0_f64,
stir in 0.5..1.0_f64,
) {
let result = simulate(h2o2_pct, kmno4_mM, vol_mL, T_start_C, stir);
prop_assert!(result.T_peak_C < 70.0);
prop_assert!(result.completed);
prop_assert!(result.O2_volume_mL > 0.0);
}
#[test]
fn unsafe_envelope_caught(
h2o2_pct in 20.0..50.0_f64,
kmno4_mM in 50.0..100.0_f64,
vol_mL in 50.0..500.0_f64,
stir in 0.0..0.2_f64,
) {
let result = simulate(h2o2_pct, kmno4_mM, vol_mL, 25.0, stir);
let envelope_check = check_safety_envelope(h2o2_pct, kmno4_mM, vol_mL, stir);
prop_assert!(!envelope_check.passes);
}
}7 What this gives the prac
Three useful artifacts emerge from this exercise:
The first is a written safety case rather than a list of safety rules. The case is: given conservation laws, given the kinetic constants, given the envelope, the safety theorems hold. The rules (“wear glasses”, “use the water bath”) are derived from the theorems, not asserted independently.
The second is traceability. If a student asks “why 6% not 9%?”, the answer is in the envelope predicate, which traces to the temperature bound, which traces to the kinetic constants and the conservation laws. The prac’s design decisions are auditable.
The third is transferability. The same specification pattern, with different numbers, describes industrial H₂O₂ handling, propellant systems, and pulp-bleaching plants. The Year 10 prac is a small instance of a structure that scales to defence-grade safety cases. Students who internalise this pattern have learned something about how engineering works, not just something about one reaction.
This is also why the Helios architectural pattern — typed graph as engine, ActionLegs as trust primitive, governed transitions — applies as cleanly to a chemistry prac as to a software system. Both are processes with conservation laws, envelopes, and consequences for envelope violation. The reactor and the runtime are isomorphic.