White paper · bil v0.6.0 · October 2026

Bounded Invariant Logic in Practice

Proving the safety logic of fourteen industrial, medical and security designs before they run, with every requirement traced to a qualified source.

bil projectModels: examples/domains/Sources: docs/whitepaper/CITATIONS.md

Abstract

Accident and recall investigations keep finding the same class of defect: interlocks, alarms and protocol state machines whose logic was wrong in the design, long before any code ran. bil (Bounded Invariant Logic) is a statically typed language that puts domain ontologies, first-order specifications, Dijkstra's guarded commands and reactive state machines in one source file, and checks them with weakest-precondition proofs, SMT solving and explicit-state model checking. The same file then runs on an interpreter, a bytecode VM or as a native binary.

This paper applies bil to fourteen domains, from semiconductor anneal control after spectroscopic ellipsometry to surgical teleoperation, process safety instrumented systems and TLS-style handshakes. Each model encodes requirements taken from standards, regulator reports and peer-reviewed physics, and each source is graded and cited. Across the suite, z3 proves all 147 verification obligations with none left to sampling, the model checker explores 518 states in 16 systems and proves 14 liveness properties, and all three execution back ends print identical results. Eleven one-line seeded bugs, each modeled on a documented failure mode, are all caught with a concrete counterexample. The research also corrected four of our own first drafts, which is the strongest argument in the paper for tying formal models to primary sources.

14domain models
147obligations proved by z3
0left to bounded sampling
518states explored in 16 systems
10 / 10seeded bugs caught
3back ends with identical output

Figures are generated from live runs of bil verify and bil model-check when this page is built, and the same checks run in tests/domain_examples.rs.

1Why designs fail

The failures that matter most in safety-critical systems are rarely arithmetic slips. They are logic errors in how a system reacts to events: an alarm that does not latch, a state machine that accepts a message out of order, an interlock that is correct for each fault alone but not for two faults together.

  • Medical devices. Between 2005 and 2009 the FDA received about 56,000 adverse-event reports for infusion pumps and oversaw 87 recalls, 14 of them Class I. Its analysis traced many problems to design and engineering, including software defects such as failures of built-in safety alarms [fda_ipii].
  • Process plants. The U.S. Chemical Safety Board found that the 2007 T2 Laboratories explosion, which killed four employees and injured 28 people at nearby businesses, was a runaway reaction that most likely followed an inadequate reactor cooling system [csb_t2].
  • Security protocols. Systematic testing of TLS libraries found state-machine bugs that had gone unnoticed for years, including SKIP-TLS and FREAK, where a network attacker could skip handshake messages. The authors trace them to incorrect compositions of individually correct state machines [beurdouche2015, ncc_smack].

Industry has shown that this class of error can be found before deployment. Amazon Web Services has model-checked the designs of critical systems since 2011 and reports finding subtle bugs that testing missed [newcombe2015]. Tools such as SPIN [holzmann1997], which made model checking of protocols like Peterson's mutual exclusion [peterson1981] routine, TLA+, Alloy and Verus [lattuada2023] are mature. The barrier is that the domain model, the specification, the protocol model and the executable logic usually live in different tools and drift apart.

2The language and toolchain

bil keeps all four in one file. A program can contain:

  • Ontology: concept hierarchies with <: subtyping, algebraic data types, and first-order axioms over them.
  • Specified functions: fn with requires and ensures, written in Dijkstra's guarded command language [dijkstra1975]: if … fi with nondeterministic choice among enabled guards, and do … od loops with an invariant and a variant.
  • Reactive systems: system blocks with typed state, safety invariants, temporal properties (P ~> Q, eventually), an optional terminal condition and interleaved guarded transitions in the style of SPIN/Promela.
  • Data pipelines: |> chains of where, map, sort_by, sum and quantifiers over concrete data.
flowchart LR
  SRC["model.bil"] --> CHK["check: ontology DAG + Hindley-Milner types"]
  CHK --> WP["verify: weakest preconditions"]
  WP --> SMT["z3 / cvc5: PROVED or counterexample values"]
  WP --> BND["bounded sampler: cross-check"]
  CHK --> MC["model-check: BFS + Tarjan SCC + weak fairness"]
  CHK --> EX["run / vm / build: ghost-erased execution"]
  CHK --> VER["emit-verus: Verus Rust"]

Verification conditions

For if G₁ → S₁ [] … [] Gₙ → Sₙ fi, bil verify generates guard totality (some guard holds under the precondition) and one obligation per branch, Gᵢ ⇒ wp(Sᵢ, Q). Because the semantics is demonic, a design with overlapping guards must be correct whichever enabled branch runs. For a do … od loop it generates five obligations: invariant initialization, preservation by every branch, non-negativity and strict decrease of the variant, and the postcondition on exit. The formal rules are in docs/SEMANTICS.md.

Each obligation ends in one of three verdicts:

  • PROVED (by z3): the SMT solver [demoura2008] showed the negated condition unsatisfiable.
  • REFUTED: a counterexample, with concrete values recovered from the solver's model, for example { x = 37 }.
  • BOUNDED (n samples): only sampled, either every combination of the parameters' sample values or, when there are more than 10,000, 10,000 of them, chosen to cover every pair of parameter values where that fits, shown as n of m samples. bil verify exits with status 1 in that case unless --allow-bounded is given, so sampled evidence is never mistaken for a proof.

Model checking

bil model-check explores every reachable state of a system breadth-first, so each counterexample is a shortest trace. It checks every invariant in every state, reports a deadlock wherever no guard is enabled in a non-terminal state, and checks P ~> Q by decomposing the ¬Q subgraph into strongly connected components under weak fairness: a cycle only counts as a violation if no transition that leaves it stays enabled throughout. Liveness counterexamples are printed as lassos.

Execution

Proof-only constructs are erased before execution. The tree-walking interpreter, the bytecode VM and native binaries built through rustc share checked 64-bit arithmetic, Euclidean division, and limits of 64 nested calls and 100,000 loop steps; differential tests require identical output from all three. At run time, axioms are checked over the concept instances that actually exist (a closed world), while in the SMT encoding they hold over all models (an open world).

3Method

Each use case went through the same six steps.

  1. Draft the model from domain knowledge.
  2. Research and qualify sources. Every requirement, limit or physical constant is traced to a source and graded: A for standards, specifications and regulators; B for peer-reviewed work; C for manufacturer documents and patents; D for secondary sources used only to corroborate. Each entry also records how much of it was actually read. Several standards (ISO 10218, 13851, 13855 and 15622, and IEC 61511) are paywalled. Their figures come from secondary quotations and are marked as such.
  3. Encode each requirement as a contract, loop invariant, system invariant or temporal property, citing its key inline in the source file.
  4. Check with bil verify, bil model-check and all three back ends.
  5. Seed a bug. Each lesson gets a one-line variant in examples/domains/seeded_bugs/ that reproduces a documented failure mode. bil must reject it with a specific counterexample.
  6. Regress. tests/domain_examples.rs requires every model to be fully proved and every seeded bug to be caught. It runs in about nine seconds as part of the local CI gate.

The research corrected four first drafts. The SPE regrowth rates were low by about 15–20%; sensor plausibility used an arbitrary span instead of the NAMUR NE 43 failure bands; the ACC model used a "two-second rule" where the sources give standard minimum time gaps of 0.8–1 s and recommend 1–2 s; and the bank-angle protection forced a roll-back even while the pilot held the stick, which is not how normal law behaves. The model checker also corrected one draft: an MQTT model whose retransmission guard was too strict to expose the bug it was written to show.

4Results

Every model below verifies with all obligations proved by SMT, model-checks without violation, and gives the same output under the interpreter, the VM and a native build. Verifying and model-checking the whole suite takes under two seconds with a release build.

Use caseModelFunctionsObligations provedBounded onlySystemsStates exploredLTL proved
Semiconductor: SE-gated SPE annealsemiconductor_se_spe.bil525013681
Process safety: reactor SISprocess_safety_reactor.bil2201231
Robotics: cobot SSM cellrobotics_cobot_cell.bil280161
Surgical robotics: teleoperationsurgical_teleoperation.bil390171
Medical devices: PCA infusion pumpmedical_infusion_pump.bil2901111
Manufacturing: press guardingmanufacturing_press_cell.bil31001131
IIoT: MQTT QoS 2 and NE 43iiot_mqtt_qos2.bil2801210
Control: anti-windup PIcontrol_antiwindup_pi.bil32201122
Navigation: geofence and RTHnavigation_geofence.bil3160181
Automotive: adaptive cruiseautomotive_acc.bil2701110
Aerospace: envelope protectionaerospace_envelope.bil2120181
Energy storage: BMSenergy_bms_balancing.bil2120160
Public safety: signals and crossingpublic_safety_traffic_rail.bil1102113
Cybersecurity: zero trustcybersecurity_zero_trust.bil2602131
Total14 models3414701651814

Eleven seeded bugs, each caught:

Seeded bugWhat changedHow bil rejects it
spe_late_cutoffRegrowth bookkeeping step not held back after the SE signal is latched, so the cut-off misses its 3 ms deadlineVIOLATION Deadline_CutOnDetect, 14-step trace
spe_slow_thermal_loopThermal loop one tick too slow during an over-temperature excursionVIOLATION NeverMeltAmorphousSi, 11-step trace
spe_overtemp_only_in_soakOver-strict invariantVIOLATION OverTempIsTransient via a pyrometer fault
reactor_slow_sisHeating not pre-empted at the trip pointVIOLATION BelowDesignTemperature, temp = 9
mqtt_unordered_transportPUBREL may overtake a PUBLISHVIOLATION ExactlyOnceSafety, delivered = 2
tls_early_finishedClient accepts an injected early FinishedVIOLATION NoDataToUnverifiedPeer
bms_fault_always_opensIgnores contactor weldingVIOLATION FaultOpensPack via Closed → Welded
robotics_stop_always_clearsClaims the protective stop always clearsLTL FAILED fair lasso
infusion_alarm_always_clearedClaims every alarm is eventually clearedLTL FAILED fair lasso of recurring hazards
cyber_noncompliant_grantIssues a self-approved production grantRuntimeError axiom SeparationOfDuties
reactor_trip_shared_inputTransmitter 3 wired to two voter inputs in place of transmitter 2REFUTED high_temp_trip, through the unfolded call to vote_2oo3

5Use cases

Each use case gives the context and its sources, what was modeled, what was proved, and what the checker found. Code excerpts are copied from the model files when this page is built.

Semiconductor manufacturing · lead case

Spectroscopic ellipsometry gating a solid-phase epitaxy anneal

25 obligations proved158 statesAnnealFinishes LTL proved2 seeded bugs caughtsemiconductor_se_spe.bil

Process context

Ion implantation amorphizes a surface layer of a silicon wafer. A thermal anneal then regrows it epitaxially from the crystalline substrate below: solid-phase epitaxy (SPE). Two measurements and one control loop decide whether the result is single-crystal silicon.

  • Metrology before the anneal. Spectroscopic ellipsometry measures the change in polarization, Ψ and Δ, over wavelength [fujiwara2007]. Fitting a multilayer optical model (oxide, amorphous layer, damaged substrate) gives the amorphous layer thickness. The fit has to be trusted with care: with an unsuitable dielectric-function model, ellipsometry can overestimate low-level damage [lohner1996]. SE has been used to follow the regrowth of implant-amorphized silicon [holgado1995].
  • Kinetics of the regrowth. For intrinsic Si the regrowth front moves at v = 4.64×10¹⁶ Å/s · exp(−2.7 eV / kT) [roth1990, johnson2007]. That is about 1.4 Å/s at 550 °C, 12 Å/s at 600 °C and 84 Å/s at 650 °C, so 30 °C of error changes the anneal time by a factor of two or more. Random nucleation in the amorphous layer has a higher activation energy, about 4 eV, so it gains on epitaxy as temperature rises [olsonroth1988, olson1985]. This sets the upper edge of the process window.
  • The thermal hazard. Amorphous Si melts 200 ± 50 K below crystalline Si. Under pulsed heating, a thin liquid layer can then propagate through the amorphous film at 10–20 m/s and leave fine-grained polycrystalline silicon: explosive crystallization [thompson1984]. In rapid thermal processing, temperature non-uniformity during ramps causes slip, which limits how fast the lamps may slew [norman1991, uspto6403925]. Typical RTP ramps run at 20–100 °C/s [uspto6034356].
  • In-situ monitoring. Real-time SE during solid-phase crystallization yields both a near-surface temperature calibration and the crystalline volume fraction over time [fujiwara1998]. This makes an ellipsometric endpoint for the regrowth, and a second temperature channel, practical.
stateDiagram-v2
  [*] --> Load
  Load --> Measure: amorphous layer of 3 units
  Measure --> Ramp: SE fit valid (se_ok)
  Measure --> Reject: SE fit rejected
  Ramp --> Soak: temp reaches window (band 6)
  Ramp --> Cool: pyrometer fault, lamp off
  Soak --> Soak: regrow one unit, or excursion to band 7 and back
  Soak --> Cool: SE endpoint (amorph = 0), lamp off
  Soak --> Cool: pyrometer fault, lamp off
  Cool --> Done: cold and fully regrown
  Cool --> Reject: cold with amorphous layer left

What is modeled and proved

The SE gate accepts a site only when the regression converged, the fit error is under a threshold, and the thickness is inside the implant recipe's expected range. z3 proves the gate is exactly that predicate, with no hidden case:

fn se_site_valid(s: SeSite, mse_max: Int, t_min: Int, t_max: Int) -> Bool
  requires mse_max > 0 && 0 <= t_min && t_min < t_max
  ensures  result <=> (s.converged && s.mse_milli <= mse_max
                       && s.a_si_thickness_a >= t_min && s.a_si_thickness_a <= t_max)
=
  s.converged && s.mse_milli <= mse_max
  && s.a_si_thickness_a >= t_min && s.a_si_thickness_a <= t_max

The wafer disposition is proved for all inputs: fewer than 80% usable sites always sends the wafer back to metrology, and enough sites with a uniform layer always releases it. The regrowth-rate table comes from the Arrhenius law above. Each band uses the rate at its lower edge, so a time computed from it is never optimistic, and z3 proves the rate is zero outside the window and positive inside:

fn spe_rate(temp_c: Int, t_upper: Int) -> Int
  requires t_upper > 650
  ensures  result >= 0 && (temp_c < 550 => result == 0) && (temp_c >= t_upper => result == 0)
           && (temp_c >= 550 && temp_c < t_upper => result > 0)
=
  if temp_c < 550                          -> 0
  [] temp_c >= 550 && temp_c < 600         -> 1
  [] temp_c >= 600 && temp_c < 650         -> 12
  [] temp_c >= 650 && temp_c < t_upper     -> 84
  [] temp_c >= t_upper                     -> 0
  fi

The fast thermal loop is where the hazards meet. Whatever the outer loop demands, the per-tick setpoint stays within the slew limit and never exceeds the hard temperature limit. All five branches are proved, including the case where the demand is above the hard limit while the current setpoint is below it:

fn thermal_setpoint(cur: Int, demand: Int, max_step: Int, t_hard: Int) -> Int
  requires max_step > 0 && cur <= t_hard
  ensures  result <= t_hard && result - cur <= max_step && cur - result <= max_step
=
  if demand > cur + max_step && cur + max_step <= t_hard   -> cur + max_step
  [] demand > cur + max_step && cur + max_step > t_hard    -> t_hard
  [] demand < cur - max_step                               -> cur - max_step
  [] demand >= cur - max_step && demand <= cur + max_step && demand <= t_hard -> demand
  [] demand >= cur - max_step && demand <= cur + max_step && demand > t_hard  -> t_hard
  fi

The anneal itself is a system with temperature in bands. Lamp drift or latent-heat release may push the wafer out of the window at any time during the soak, up to a bounded number of excursions, and the pyrometer may fail at any point. Five invariants are checked in all 158 reachable states, and AnnealFinishes proves under weak fairness that every anneal that starts ramping ends in Done or Reject:

  invariant NeverMeltAmorphousSi:   temp <= 7
  invariant NoAnnealWithoutSe:      (phase == Ramp || phase == Soak) => se_ok
  invariant NoHeatOnPyrometerFault: !pyro_ok => !lamp
  invariant RegrowthOnlyAfterSe:    amorph < 3 => se_ok || phase == Load || phase == Measure
  // Over-temperature only arises from a soak excursion. A pyrometer fault in the middle
  // of one drops straight to Cool with the lamp off, so the wafer can still be at
  // band 7 in Cool (the model checker found that trace for a stricter `phase == Soak`).
  invariant OverTempIsTransient:    temp == 7 => ((phase == Soak || phase == Cool) && excursions >= 1)

On the example wafer W07 the verdict is Rework. Only three of five sites pass the SE gate, which is under 80%, even though the three good thicknesses are uniform (uniform = true, mean 411 Å). At 600 °C that layer needs 35 one-second ticks to regrow, computed by regrowth_ticks, which is proved to terminate with the whole layer consumed.

What the checker found

A thermal loop one tick too slow melts the amorphous layer. If the controller can heat once more while already in the over-temperature band, the wafer reaches band 8, which is the a-Si melt and explosive-crystallization hazard. The checker returns the shortest path to it:

$ bil model-check examples/domains/seeded_bugs/spe_slow_thermal_loop.bil   # exit 1
  [VIOLATION] Safety Invariant 'NeverMeltAmorphousSi' violated at state { amorph=3; excursions=1; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=8 }
    Init: { amorph=0; excursions=0; lamp=false; phase=Load; pyro_ok=true; se_ok=false; temp=0 }
    Step 1 [Guard #1 (phase == Load)] -> { amorph=3; excursions=0; lamp=false; phase=Measure; pyro_ok=true; se_ok=false; temp=0 }
    Step 2 [Guard #2 (phase == Measure)] -> { amorph=3; excursions=0; lamp=false; phase=Ramp; pyro_ok=true; se_ok=true; temp=0 }
    Step 3 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=1 }
    Step 4 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=2 }
    Step 5 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=3 }
    Step 6 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=4 }
    Step 7 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=5 }
    Step 8 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=6 }
    Step 9 [Guard #5 ((phase == Ramp) && (temp == 6))] -> { amorph=3; excursions=0; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=6 }
    Step 10 [Guard #7 (((phase == Soak) && (temp == 6)) && (excursions < 2))] -> { amorph=3; excursions=1; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=7 }
    Step 11 [Guard #9 (((phase == Soak) && (temp == 7)) && lamp)] -> { amorph=3; excursions=1; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=8 }

An invariant that was too strong. The first draft stated that over-temperature can only occur during the soak. The checker showed a pyrometer fault in the middle of an excursion: the lamp is cut and the phase moves to Cool while the wafer is still in band 7. Cutting the lamp is the right response, so the invariant was corrected rather than the design.

$ bil model-check examples/domains/seeded_bugs/spe_overtemp_only_in_soak.bil   # exit 1
  [VIOLATION] Safety Invariant 'OverTempIsTransient' violated at state { amorph=3; excursions=1; lamp=false; phase=Cool; pyro_ok=false; se_ok=true; temp=7 }
    Init: { amorph=0; excursions=0; lamp=false; phase=Load; pyro_ok=true; se_ok=false; temp=0 }
    Step 1 [Guard #1 (phase == Load)] -> { amorph=3; excursions=0; lamp=false; phase=Measure; pyro_ok=true; se_ok=false; temp=0 }
    Step 2 [Guard #2 (phase == Measure)] -> { amorph=3; excursions=0; lamp=false; phase=Ramp; pyro_ok=true; se_ok=true; temp=0 }
    Step 3 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=1 }
    Step 4 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=2 }
    Step 5 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=3 }
    Step 6 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=4 }
    Step 7 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=5 }
    Step 8 [Guard #4 (((phase == Ramp) && pyro_ok) && (temp < 6))] -> { amorph=3; excursions=0; lamp=true; phase=Ramp; pyro_ok=true; se_ok=true; temp=6 }
    Step 9 [Guard #5 ((phase == Ramp) && (temp == 6))] -> { amorph=3; excursions=0; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=6 }
    Step 10 [Guard #7 (((phase == Soak) && (temp == 6)) && (excursions < 2))] -> { amorph=3; excursions=1; lamp=true; phase=Soak; pyro_ok=true; se_ok=true; temp=7 }
    Step 11 [Guard #10 (((phase == Ramp) || (phase == Soak)) && pyro_ok)] -> { amorph=3; excursions=1; lamp=false; phase=Cool; pyro_ok=false; se_ok=true; temp=7 }

Limits. Temperature is discretized into bands and time into ticks. A production controller needs dense-time or hybrid analysis of the plant, and the window edge (680 °C here), the fit thresholds and the excursion budget are example recipe parameters, not recommendations. The model proves the supervisory logic and the per-tick command bounds, not the thermal physics.

Critical process systems

A safety instrumented system for an exothermic reactor

2 obligations proved23 statesTripIsReset LTL proved2 seeded bugs caught

The T2 Laboratories explosion was a runaway reaction after a cooling failure [csb_t2]. A safety instrumented system under IEC 61511 [iec61511] is the independent layer meant to stop that sequence. Three temperature transmitters voted 2-out-of-3 tolerate one fault both against failing to trip and against tripping spuriously [lundteigen_sis], at a higher cost and complexity than simpler architectures [kenexis_2oo3]. Both properties are proved for all inputs:

fn vote_2oo3(a: Bool, b: Bool, c: Bool) -> Bool
  requires true
  ensures  result <=> ((a && b) || (a && c) || (b && c))
=
  (a && b) || (a && c) || (b && c)

// High-temperature trip with three redundant transmitters (deci-degrees C).
// Proved: a single failed-low transmitter cannot block the trip, and a single
// failed-high transmitter cannot cause a spurious one.
fn high_temp_trip(t1: Int, t2: Int, t3: Int, setpoint: Int) -> Bool
  requires setpoint > 0
  ensures  ((t1 >= setpoint && t2 >= setpoint) => result)
           && ((t1 < setpoint && t2 < setpoint) => !result)
=
  vote_2oo3(t1 >= setpoint, t2 >= setpoint, t3 >= setpoint)

The reactor system lets cooling fail at any time. While running, the SIS trips at band 7 and pre-empts further heating, residual heat may add one more step, and the reactor is reset after cooling. The design temperature is never exceeded, and every trip is eventually reset.

What the checker found

If heating is not pre-empted at the trip point, which is what happens when the SIS responds more slowly than the reaction, the interleaving lets the temperature climb past the design limit before the trip fires:

$ bil model-check examples/domains/seeded_bugs/reactor_slow_sis.bil   # exit 1
  [VIOLATION] Safety Invariant 'BelowDesignTemperature' violated at state { cooling=false; feed=true; residual=false; temp=9; tripped=false }
    Init: { cooling=true; feed=true; residual=false; temp=5; tripped=false }
    Step 1 [Guard #4 (cooling && !(tripped))] -> { cooling=false; feed=true; residual=false; temp=5; tripped=false }
    Step 2 [Guard #1 ((feed && !(cooling)) && (temp < 10))] -> { cooling=false; feed=true; residual=false; temp=6; tripped=false }
    Step 3 [Guard #1 ((feed && !(cooling)) && (temp < 10))] -> { cooling=false; feed=true; residual=false; temp=7; tripped=false }
    Step 4 [Guard #1 ((feed && !(cooling)) && (temp < 10))] -> { cooling=false; feed=true; residual=false; temp=8; tripped=false }
    Step 5 [Guard #1 ((feed && !(cooling)) && (temp < 10))] -> { cooling=false; feed=true; residual=false; temp=9; tripped=false }

Limits. Response time is abstracted as transition priority. Probability of failure on demand, proof-test intervals and common-cause failure, which IEC 61511 requires, are outside the model.

Collaborative robotics

Speed and separation monitoring in a cobot cell

8 obligations proved6 statesEStopIsReleasable LTL proved1 seeded bug caught

ISO/TS 15066 defines speed and separation monitoring (SSM) as one of four collaborative modes [isots15066]. NIST has published guidance on implementing its protective separation distance [marvel2017] and built a laser-scanner testbed that stops and restarts a robot from it [szabo2012]. The model takes the protective distance as an input and adds a 500 mm collaborative band capped at the 250 mm/s reduced speed associated with ISO 10218 [iso10218]:

fn ssm_speed_limit(sep_mm: Int, protective_mm: Int, vmax: Int) -> Int
  requires protective_mm > 0 && vmax >= 250 && sep_mm >= 0
  ensures  result >= 0 && result <= vmax
           && (sep_mm <= protective_mm => result == 0)
           && (sep_mm < protective_mm + 500 => result <= 250)
=
  if sep_mm <= protective_mm                                  -> 0
  [] sep_mm > protective_mm && sep_mm < protective_mm + 500   -> 250
  [] sep_mm >= protective_mm + 500                            -> vmax
  fi

The cell supervisor lets the human move between zones at any moment, with the scanner's safety output acting in the same step. Four invariants hold in every state: standstill in the protective zone, reduced speed in the shared band, E-stop means stop, and a valid zone.

What the checker found

The first draft claimed that a protective stop always clears. It cannot, because the human may stay in the protective zone, or press E-stop again, forever. The checker returns that as a fair lasso. What the controller can promise is that a latched E-stop is always releasable, and that is now proved.

$ bil model-check examples/domains/seeded_bugs/robotics_stop_always_clears.bil   # exit 1
  [LTL FAILED] temporal `StopIsNotPermanent`: ((mode == ProtectiveStop) && !(estop)) ~> (mode != ProtectiveStop)
  [VIOLATION] LTL Temporal Property 'StopIsNotPermanent' (((mode == ProtectiveStop) && !(estop)) ~> (mode != ProtectiveStop)) violated at state { estop=true; mode=ProtectiveStop; speed=0; zone=2 }
    Init: { estop=false; mode=Auto; speed=1000; zone=0 }
    Step 1 [Guard #1 ((zone == 0) && !(estop))] -> { estop=false; mode=Reduced; speed=250; zone=1 }
    Step 2 [Guard #2 ((zone == 1) && !(estop))] -> { estop=false; mode=ProtectiveStop; speed=0; zone=2 }
    Step 3 [Guard #5 !(estop)] -> { estop=true; mode=ProtectiveStop; speed=0; zone=2 }
    Weakly Fair ¬Q Cycle (Lasso): { estop=true; mode=ProtectiveStop; speed=0; zone=2 } -> { estop=false; mode=ProtectiveStop; speed=0; zone=2 }

Surgical robotics

Teleoperation with virtual fixtures and a link watchdog

9 obligations proved7 statesHoldIsLeftWhenLinkIsUp LTL proved

Virtual fixtures, introduced for telepresence by Rosenberg [rosenberg1993], include forbidden-region fixtures that keep a manipulator out of parts of the workspace. They have been studied on the da Vinci and JHU Steady-Hand platforms [abbott2007]. Robotically assisted surgical equipment falls under IEC 80601-2-77 [iec80601277]. The model proves three instrument-level functions: a depth fixture that never lets the tip pass the limit while leaving retraction unrestricted, 5:1 motion scaling, and a symmetric force limit.

fn fixture_step(depth: Int, step: Int, limit: Int) -> Int
  requires depth <= limit
  ensures  depth + result <= limit
           && (step <= 0 => result == step)
           && (step > 0 => (result >= 0 && result <= step))
=
  if step <= 0                             -> step
  [] step > 0 && depth + step <= limit     -> step
  [] step > 0 && depth + step > limit      -> limit - depth
  fi

The supervisor puts the arm on hold when the console link drops. When the link returns, the arm stays on hold until the surgeon releases and re-presses the clutch. NoMotionWithoutReengage is checked in every state, because motion that resumes on its own when the link recovers is the hazard.

Medical devices

A patient-controlled analgesia infusion pump

9 obligations proved11 statesClearPumpCanRun LTL proved1 seeded bug caught

The FDA's Infusion Pump Improvement Initiative cites failures of built-in safety alarms among recurring defects [fda_ipii]. The FDA's Generic PCA pump model and its safety requirements have been model-checked in UPPAAL by others [kim2011gpca, gpca_umn]. This model proves the bolus rule (lockout interval and hourly cap, stated as an exact equivalence) and that delivery never exceeds the volume to be infused and stops exactly on it. The interlock system checks no free flow with the door open, a stop on occlusion or air-in-line, and an alarm that latches the motor off.

fn infuse(vtbi: Int, stroke: Int) -> Int
  requires vtbi >= 0 && stroke > 0
  ensures  result == vtbi
=
  do v = 0
    invariant v >= 0 && v <= vtbi
    variant   vtbi - v
  :
     vtbi - v >= stroke             -> v := v + stroke
  [] vtbi - v < stroke && v < vtbi  -> v := vtbi
  od
  then v

What the checker found

"Every alarm is eventually cleared" does not hold. Hazards can keep recurring, and clearing an alarm is a clinical action rather than something the pump controls. The checker returns a fair lasso of alternating occlusion, air and door faults:

$ bil model-check examples/domains/seeded_bugs/infusion_alarm_always_cleared.bil   # exit 1
  [LTL FAILED] temporal `AlarmsAreAcknowledged`: alarm ~> !(alarm)
  [VIOLATION] LTL Temporal Property 'AlarmsAreAcknowledged' (alarm ~> !(alarm)) violated at state { air=false; alarm=true; door_closed=false; occlusion=true; pumping=false }
    Init: { air=false; alarm=false; door_closed=true; occlusion=false; pumping=false }
    Step 1 [Guard #3 !(occlusion)] -> { air=false; alarm=true; door_closed=true; occlusion=true; pumping=false }
    Step 2 [Guard #5 (door_closed && !(pumping))] -> { air=false; alarm=true; door_closed=false; occlusion=true; pumping=false }
    Weakly Fair ¬Q Cycle (Lasso): { air=false; alarm=true; door_closed=false; occlusion=true; pumping=false } -> { air=false; alarm=true; door_closed=false; occlusion=false; pumping=false } -> { air=false; alarm=true; door_closed=true; occlusion=false; pumping=false } -> { air=true; alarm=true; door_closed=true; occlusion=false; pumping=false } -> { air=true; alarm=true; door_closed=false; occlusion=false; pumping=false } -> { air=true; alarm=true; door_closed=false; occlusion=true; pumping=false } -> { air=true; alarm=true; door_closed=true; occlusion=true; pumping=false } -> { air=false; alarm=true; door_closed=true; occlusion=true; pumping=false }

Manufacturing

Hydraulic press guarding and gravimetric dosing

10 obligations proved13 statesNoStuckDownstroke LTL proved

Two-hand control under ISO 13851 type III requires both actuators within 0.5 s, and both released before re-triggering [iso13851]. A light curtain must be mounted at least S = K·T + C from the hazard, with K = 2000 mm/s and C = 8(d − 14) for resolutions d ≤ 40 mm [iso13855]. Sources disagree on when K may drop to 1600 mm/s, so the model always uses the larger distance:

fn light_curtain_distance(t_stop_ms: Int, d_mm: Int) -> Int
  requires t_stop_ms > 0 && d_mm >= 14 && d_mm <= 40
  ensures  result == 2 * t_stop_ms + 8 * (d_mm - 14) && result >= 2 * t_stop_ms
=
  2 * t_stop_ms + 8 * (d_mm - 14)

The press system lets either hand release, the curtain break or the door open during the down-stroke, and the safety relay reverses the ram in the same step. DownstrokeIsGuarded holds in every state, and every down-stroke returns to the top. Coarse/fine dosing is proved never to overfill and to end exactly on target.

Industrial IoT

MQTT exactly-once delivery and NAMUR NE 43 telemetry

8 obligations proved21 states1 seeded bug caught

The model sends one QoS 2 PUBLISH over a network that may lose any packet, with timeout retransmission at the sender. MQTT 3.1.1 requires the receiver to acknowledge re-sent PUBLISHes until PUBREL and "MUST NOT cause duplicate messages to be delivered" [MQTT-4.3.3-2], and it assumes "an ordered, lossless, stream of bytes" underneath (§4.2) [mqtt311]. The sender side keeps its copy until PUBREC and the packet identifier until PUBCOMP [emqx_qos]. With an in-order transport, the model checker shows at most one delivery in every state and delivery whenever the sender reaches Done.

What the checker found

Drop the ordering assumption, so that PUBREL can overtake a retransmitted PUBLISH, and the receiver releases the packet identifier before the duplicate arrives. The duplicate is then delivered as new. The protocol's exactly-once guarantee depends on the transport, and the model makes that dependency explicit:

$ bil model-check examples/domains/seeded_bugs/mqtt_unordered_transport.bil   # exit 1
  [VIOLATION] Safety Invariant 'ExactlyOnceSafety' violated at state { delivered=2; net_comp=true; net_pub=false; net_rec=true; net_rel=false; s=WaitComp; stored=true }
    Init: { delivered=0; net_comp=false; net_pub=false; net_rec=false; net_rel=false; s=SendPub; stored=false }
    Step 1 [Guard #1 (s == SendPub)] -> { delivered=0; net_comp=false; net_pub=true; net_rec=false; net_rel=false; s=WaitRec; stored=false }
    Step 2 [Guard #4 (net_pub && !(stored))] -> { delivered=1; net_comp=false; net_pub=false; net_rec=true; net_rel=false; s=WaitRec; stored=true }
    Step 3 [Guard #2 ((s == WaitRec) && !(net_pub))] -> { delivered=1; net_comp=false; net_pub=true; net_rec=true; net_rel=false; s=WaitRec; stored=true }
    Step 4 [Guard #7 (net_rec && (s == WaitRec))] -> { delivered=1; net_comp=false; net_pub=true; net_rec=false; net_rel=true; s=WaitComp; stored=true }
    Step 5 [Guard #11 net_rel] -> { delivered=1; net_comp=true; net_pub=true; net_rec=false; net_rel=false; s=WaitComp; stored=false }
    Step 6 [Guard #4 (net_pub && !(stored))] -> { delivered=2; net_comp=true; net_pub=false; net_rec=true; net_rel=false; s=WaitComp; stored=true }

The same file classifies 4–20 mA loop currents under NAMUR NE 43: 3.8–20.5 mA is a measurement, and ≤ 3.6 mA or ≥ 21 mA signals a failure [namur_ne43]. The classification is proved for every input and drives a telemetry pipeline that flags ["PT-102", "PT-103"] as failed and ["PT-104"] as suspect.

fn ne43_class(ua: Int) -> Ne43
  requires true
  ensures  (ua >= 3800 && ua <= 20500 => result == Measurement)
           && ((ua <= 3600 || ua >= 21000) => result == Failure)
           && ((ua > 3600 && ua < 3800) || (ua > 20500 && ua < 21000) => result == Warning)
=
  if ua >= 3800 && ua <= 20500                              -> Measurement
  [] ua <= 3600 || ua >= 21000                              -> Failure
  [] (ua > 3600 && ua < 3800) || (ua > 20500 && ua < 21000) -> Warning
  fi

Control systems

Fixed-point PI control with anti-windup

22 obligations proved12 states2 LTL proved

When an actuator saturates, an integrator keeps accumulating and the loop behaves as if open. Conditional integration and back-calculation are the two standard remedies [scilab_aw, astrom_murray]. The model proves, for all integer inputs as on a PLC, that saturation stays in the actuator range, that the conditionally integrated state stays bounded, and that a rate-limited setpoint ramp never overshoots and lands exactly on target:

fn ramp_to(start: Int, target: Int, rate: Int) -> Int
  requires rate > 0
  ensures  result == target
=
  do r = start
    invariant (start <= target => (r >= start && r <= target))
              && (start > target => (r <= start && r >= target))
    variant   abs(target - r)
  :
     r < target && target - r > rate  -> r := r + rate
  [] r < target && target - r <= rate -> r := target
  [] r > target && r - target > rate  -> r := r - rate
  [] r > target && r - target <= rate -> r := target
  od
  then r

A hysteresis thermostat system keeps the temperature in its comfort band, and two liveness properties prove the heater never latches on or off.

Automotive

Adaptive cruise control with an emergency-braking override

7 obligations proved11 states

ISO 15622 covers the ACC control strategy, minimum functionality and reaction to failure [iso15622]. A review of ACC parameterization reports standard minimum selectable time gaps of 0.8 s and 1 s, and a recommended range of 1–2 s [bernsteiner2016]. The model uses 1.5 s plus a 5 m standstill margin. The acceleration request is proved to stay within comfort limits, to brake whenever the gap is short, to command emergency braking below half the safe gap, and never to accelerate above the set speed. The supervisor proves that the brake pedal always cancels ACC, and that ACC never brakes while the driver overrides with the accelerator.

fn acc_command(gap: Int, speed: Int, set_speed: Int) -> Int
  requires speed >= 0 && gap >= 0 && set_speed >= 0
  ensures  result >= 0 - 900 && result <= 200
           && (2 * gap < 3 * speed + 100 => result < 0)
           && (4 * gap < 3 * speed + 100 => result == 0 - 900)
           && (speed > set_speed => result <= 0)
=
  if 4 * gap < 3 * speed + 100                                         -> 0 - 900
  [] 4 * gap >= 3 * speed + 100 && 2 * gap < 3 * speed + 100           -> 0 - 350
  [] 2 * gap >= 3 * speed + 100 && speed > set_speed                   -> 0 - 100
  [] 2 * gap >= 3 * speed + 100 && speed <= set_speed && speed + 20 <= set_speed -> 200
  [] 2 * gap >= 3 * speed + 100 && speed <= set_speed && speed + 20 > set_speed  -> 0
  fi

Aerospace

Fly-by-wire envelope protection

12 obligations proved8 statesWarningIsCancelled LTL proved

In Airbus normal law, bank beyond 33° needs continuous sidestick input, releasing it returns the aircraft to 33°, and 67° is the limit. Between α-prot and α-max the stick commands angle of attack, and α-max is never exceeded [airbus_laws]. These figures come from secondary summaries, so the model is illustrative and the type's FCOM governs. The research corrected the first draft, which forced a roll-back even with the stick held:

fn roll_cmd(stick: Int, bank: Int) -> Int
  requires stick >= 0 - 1000 && stick <= 1000 && bank >= 0 - 6700 && bank <= 6700
  ensures  result >= 0 - 1000 && result <= 1000
           && (bank >= 6700 => result <= 0)
           && (bank <= 0 - 6700 => result >= 0)
           && (bank > 3300 && bank < 6700 && stick == 0 => result < 0)
           && (bank < 0 - 3300 && bank > 0 - 6700 && stick == 0 => result > 0)
           && (bank > 0 - 6700 && bank < 6700 && stick != 0 => result == stick)
=
  if bank >= 6700                                               -> min(stick, 0)
  [] bank <= 0 - 6700                                           -> max(stick, 0)
  [] bank > 3300 && bank < 6700 && stick == 0                   -> 0 - 100
  [] bank < 0 - 3300 && bank > 0 - 6700 && stick == 0           -> 100
  [] bank > 0 - 6700 && bank < 6700 && stick != 0               -> stick
  [] bank >= 0 - 3300 && bank <= 3300 && stick == 0             -> 0
  fi

The autopilot system proves the autopilot is engaged only inside the envelope and never with sidestick input, and that every disconnect warning is eventually cancelled.

Energy storage

Battery cell balancing and contactor sequencing

12 obligations proved6 states1 seeded bug caught

Cell balancing is proved to conserve total charge, keep both cells non-negative and terminate balanced. Charge current is proved to derate to zero outside the temperature window and to a tenth of maximum above 95% state of charge. The contactor system closes the main contactor only after precharge [uspto10476262] and models contact welding, which manufacturers detect from voltages that fail to decay after an open command [uspto11592485, uspto12077054].

fn balance(c0: CellPair) -> CellPair
  requires c0.a >= 0 && c0.b >= 0
  ensures  result.a + result.b == c0.a + c0.b
           && result.a >= 0 && result.b >= 0
           && abs(result.a - result.b) <= 1
=
  do c = c0
    invariant c.a + c.b == c0.a + c0.b && c.a >= 0 && c.b >= 0
    variant   abs(c.a - c.b)
  :
     c.a > c.b + 1 -> c := c with { a: c.a - 1, b: c.b + 1 }
  [] c.b > c.a + 1 -> c := c with { a: c.a + 1, b: c.b - 1 }
  od
  then c

What the checker found

"An isolation fault always opens the pack" is false once welding is possible. The checker produces the trace, and the trace is the engineering case for a second, independent contactor:

$ bil model-check examples/domains/seeded_bugs/bms_fault_always_opens.bil   # exit 1
  [VIOLATION] Safety Invariant 'FaultOpensPack' violated at state { iso_fault=true; k=Welded; precharged=true }
    Init: { iso_fault=false; k=Open; precharged=false }
    Step 1 [Guard #1 ((k == Open) && !(iso_fault))] -> { iso_fault=false; k=Precharge; precharged=false }
    Step 2 [Guard #2 ((k == Precharge) && !(iso_fault))] -> { iso_fault=false; k=Closed; precharged=true }
    Step 3 [Guard #6 (k == Closed)] -> { iso_fault=false; k=Welded; precharged=true }
    Step 4 [Guard #7 ((k == Welded) && !(iso_fault))] -> { iso_fault=true; k=Welded; precharged=true }

Public safety

Signals with emergency preemption, a level crossing, and dispatch triage

1 obligation proved11 states in 2 systems3 LTL proved

A conflict monitor or malfunction management unit forces an intersection into flash when it sees conflicting greens [mmu]. The MUTCD requires a steady yellow after every green and leaves red clearance to engineering practice [mutcd4d26]. The intersection model proves no conflicting greens, the property the monitor enforces in hardware, in every state, including during emergency preemption. It also proves that preemption ends and that north–south traffic is served.

The level crossing follows Heitmeyer and Lynch's Generalized Railroad Crossing benchmark [heitmeyer1994]: the gate is down whenever the crossing is occupied, and it reopens once the train has gone. The siting assumption, that the gate is down before a train can arrive, is written as an explicit guard rather than hidden. Dispatch triage is a proved scoring function and a pipeline over an incident queue.

system LevelCrossing {
  state train: Int = 0
  state gate: Gate = Up

  invariant GateDownWhenOccupied: train == 2 => gate == Down
  invariant TrainRange:           train >= 0 && train <= 2

  temporal GateReopens: (train == 0 && gate == Down) ~> (gate == Up || train == 1)

  transition
     train == 0                    -> train := 1, gate := Lowering
  [] gate == Lowering              -> gate := Down
  [] train == 1 && gate == Down    -> train := 2
  [] train == 2                    -> train := 0
  [] train == 0 && gate == Down    -> gate := Up
}

Cybersecurity

Rate limiting, lockout, handshake ordering and separation of duties

6 obligations proved13 states in 2 systemsLockoutExpires LTL proved2 seeded bugs caught

Token-bucket refill and spend are proved never to overflow capacity or go negative [rfc2697]. The lockout system uses five failures, well under NIST SP 800-63B's ceiling of 100 consecutive failures per authenticator, which permits lower limits [nist80063b], and proves that every lockout expires. The client handshake proves no application data is sent to an unverified peer. Separation of duties is an axiom over issued grants [nist80053ac5], audited by a pipeline over pending requests.

What the checker found

Accept an attacker-injected Finished straight after the hello, the SKIP-TLS pattern [beurdouche2015], and data reaches a peer whose certificate was never checked:

$ bil model-check examples/domains/seeded_bugs/tls_early_finished.bil   # exit 1
  [VIOLATION] Safety Invariant 'NoDataToUnverifiedPeer' violated at state { app_data_sent=true; cert_ok=false; hs=Finished }
    Init: { app_data_sent=false; cert_ok=false; hs=Start }
    Step 1 [Guard #1 (hs == Start)] -> { app_data_sent=false; cert_ok=false; hs=HelloSent }
    Step 2 [Guard #6 (hs == HelloSent)] -> { app_data_sent=false; cert_ok=false; hs=Finished }
    Step 3 [Guard #7 ((hs == Finished) && !(app_data_sent))] -> { app_data_sent=true; cert_ok=false; hs=Finished }

Issuing a self-approved production grant violates the axiom at run time, because axioms are enforced over the instances that actually exist:

$ bil run examples/domains/seeded_bugs/cyber_noncompliant_grant.bil   # exit 1
[RuntimeError] OntoLogic Axiom 'SeparationOfDuties' violated at line 84

6Cross-cutting lessons

  • Liveness often belongs to the environment. In the cobot cell and the infusion pump, the natural liveness claim ("the stop clears", "the alarm clears") was false, because a person or a recurring hazard controls it. The checker separates what the controller can guarantee from what it cannot, which is the distinction a hazard analysis needs.
  • Protocols carry hidden assumptions. MQTT's exactly-once guarantee is only as good as in-order transport. Writing the assumption as a guard means that deleting it produces a counterexample instead of silently weakening the proof.
  • Response time is a safety property. In the reactor and the SPE anneal, a protection function that was logically correct but one step slower than the hazard was unsafe. Interleaving semantics finds these races without a timing model, as long as the race is modeled as a choice.
  • Counterexamples also find over-strong requirements. The SPE invariant was wrong, not the design. A refuted property is a question to answer, and sometimes the answer is to fix the specification.
  • Formal models need primary sources. Four drafts changed after research, and in each case the model was internally consistent and verified before the correction. A proof shows that the model meets its specification. Only sources show that the specification matches the world.

7Limitations and threats to validity

  • Abstraction. Continuous quantities are integer bands and time is discrete steps. Claims are about supervisory logic and per-step bounds; clock and deadline state response times in whole scans of a controller. Dense-time and hybrid properties need timed or hybrid automata.
  • SMT encoding. Calls to user-defined functions are unfolded into the SMT query, together with the callee's requires and ensures checks that execution performs on every call. A recursive call to a function that declares a variant is replaced by the function's own ensures, after checking its requires and that the variant decreases; that is a proof by induction. Recursive calls to a function without a variant, and calls inside a quantifier to a function that has a contract, are not encoded, so those obligations are only bounded-checked.
  • Bounded cross-check coverage. The bounded sampler that runs beside SMT tries every combination of the parameters' sample values only while there are at most 10,000. Beyond that it evaluates 10,000 combinations, starting with a pairwise covering array, so every pair of sample values of every two parameters is tried together, and filling the rest with a fixed-seed sample. A counterexample that needs three or more parameters at particular values at once can still be missed. SMT remains the proof; the sampler is a cross-check and a source of readable counterexamples.
  • Arithmetic. SMT reasons over unbounded integers, while execution uses checked 64-bit integers that stop on overflow. Proofs therefore cover the intended mathematics, and execution fails loudly outside it.
  • Sources. Several standards were read only through secondary quotations, and those figures are marked in the citations. Parameters in the models are illustrative, not compliance values.
  • Assurance. bil is not a qualified tool under IEC 61508, ISO 26262, IEC 62304 or DO-330, and these models have not been reviewed by domain safety assessors. They demonstrate method, not certification evidence.

8Roadmap

  • A refinement path from banded models to continuous controllers, ending in Verus-checked Rust through bil emit-verus.
  • Tool-qualification evidence: requirements tracing, coverage and independent test suites for the verifier itself.

9Reproduce

Requires Rust and z3 on PATH.

cargo build --release
B=target/release/bil
for f in examples/domains/*.bil; do $B verify "$f" && $B model-check "$f" && $B run "$f"; done
$B model-check examples/domains/seeded_bugs/spe_slow_thermal_loop.bil   # exits 1 with a trace
cargo test --test domain_examples                                       # the whole suite as a test
python3 docs/whitepaper/build.py                                        # rebuild this page from live runs

References

Generated from docs/whitepaper/CITATIONS.md. Tiers: A standard, specification or regulator; B peer-reviewed or scholarly; C manufacturer or patent; D secondary, used only to corroborate.

Foundations: formal methods and tools

  1. [dijkstra1975]B

    E. W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs," CACM 18(8):453–457, 1975. https://doi.org/10.1145/360933.360975 · EWD 472 transcription: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD472.html

    Verified: abstractSupports: GCL if … fi / do … od, weakest preconditions, nondeterminism

  2. [newcombe2015]B

    C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, M. Deardeuff, "How Amazon Web Services Uses Formal Methods," CACM 58(4), 2015. https://doi.org/10.1145/2699417 · https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext

    Verified: abstractSupports: Industrial precedent: model checking designs before they ship

  3. [lattuada2023]B

    A. Lattuada et al., "Verus: Verifying Rust Programs using Linear Ghost Types," Proc. ACM Program. Lang. 7(OOPSLA1), art. 85, 2023. https://doi.org/10.1145/3586037

    Verified: abstractSupports: spec / proof / exec modes, bil emit-verus target

  4. [demoura2008]B

    L. de Moura, N. Bjørner, "Z3: An Efficient SMT Solver," TACAS 2008, LNCS 4963. https://doi.org/10.1007/978-3-540-78800-3_24

    Verified: abstractSupports: The SMT back end that discharges the obligations

  5. [holzmann1997]B

    G. J. Holzmann, "The Model Checker SPIN," IEEE TSE 23(5):279–295, 1997. https://doi.org/10.1109/32.588521

    Verified: abstractSupports: Explicit-state, interleaving-semantics model checking

  6. [peterson1981]B

    G. L. Peterson, "Myths about the mutual exclusion problem," Inf. Process. Lett. 12(3):115–116, 1981. https://doi.org/10.1016/0020-0190(81)90106-X

    Verified: abstractSupports: examples/mutex_protocol.bil

Semiconductor manufacturing: spectroscopic ellipsometry and solid-phase epitaxy

  1. [roth1990]B

    J. A. Roth, G. L. Olson, D. C. Jacobson, J. M. Poate, Appl. Phys. Lett. 57, 1340 (1990). Values as quoted in [johnson2007].

    Verified: text (via [johnson2007])Supports: Intrinsic Si SPE: v₀ = 4.64×10¹⁶ Å/s, Eₐ = 2.7 eV, which gives the spe_rate table

  2. [johnson2007]B

    B. C. Johnson, J. C. McCallum, "Dopant-enhanced solid phase epitaxy in buried amorphous silicon layers," Phys. Rev. B 76, 045216 (2007). https://doi.org/10.1103/PhysRevB.76.045216 · arXiv: https://arxiv.org/abs/1007.5372

    Verified: textSupports: Fit v₀ = (4±1)×10¹⁶ Å/s, Eₐ = 2.68±0.04 eV; time-resolved reflectivity; 460–660 °C anneals

  3. [olsonroth1988]B

    G. L. Olson, J. A. Roth, "Kinetics of solid phase crystallization in amorphous silicon," Mater. Sci. Rep. 3, 1 (1988). https://www.sciencedirect.com/science/article/pii/S0920230788800057

    Verified: secondary (search excerpt)Supports: SPE Eₐ ≈ 2.7 eV over about 470–1350 °C; random nucleation Eₐ ≈ 4 eV, so nucleation gains on SPE as temperature rises, which motivates the upper limit of the window

  4. [olson1985]B

    G. L. Olson, "Kinetics and Mechanisms of Solid Phase Epitaxy and Competitive Processes in Silicon," MRS Proc. 35, 25 (1985). https://doi.org/10.1557/PROC-35-25

    Verified: abstractSupports: Kinetic competition between SPE and random crystallization

  5. [thompson1984]B

    M. O. Thompson et al., "Melting temperature and explosive crystallization of amorphous silicon during pulsed laser irradiation," Phys. Rev. Lett. 52, 2360 (1984). https://link.aps.org/doi/10.1103/PhysRevLett.52.2360 · abstract: https://impact.ornl.gov/en/publications/melting-temperature-and-explosive-crystallization-of-amorphous-si/

    Verified: abstractSupports: a-Si melts 200±50 K below c-Si; a self-propagating liquid layer at 10–20 m/s leaves fine-grained poly-Si. This is the NeverMeltAmorphousSi hazard

  6. [lohner1996]B

    "Spectro-ellipsometric Studies of Amorphization and Thermal Annealing in Ion-implanted Silicon," Jpn. J. Appl. Phys. 35, 5929 (1996). https://doi.org/10.1143/JJAP.35.5929 · group's methods: https://ris.utwente.nl/ws/files/6689010/Lohner93ion.pdf

    Verified: abstractSupports: SE with multilayer optical models gives damaged/amorphous layer thickness. Caveat: low damage can be overestimated with unsuitable dielectric functions, which motivates the mse_milli gate

  7. [holgado1995]B

    S. Holgado, J. Martinez, J. Garrido, J. Piqueras, "Regrowth-process study of amorphous BF₂⁺ ion-implanted silicon layers through spectroscopic ellipsometry," Appl. Phys. A 60(3), 325–332 (1995). https://doi.org/10.1007/BF01538413

    Verified: abstractSupports: SE applied to the regrowth of implant-amorphized Si

  8. [fujiwara1998]B

    H. Fujiwara, J. Koh, Y. Lee, C. R. Wronski, R. W. Collins, "Real Time Spectroscopic Ellipsometry Studies of the Solid Phase Crystallization of Amorphous Silicon," MRS Proc. 507, 939 (1998). https://doi.org/10.1557/PROC-507-939

    Verified: abstractSupports: Real-time SE gives near-surface temperature calibration and crystalline volume fraction during anneal, which is the in-situ endpoint in SpeAnneal

  9. [fujiwara2007]B

    H. Fujiwara, Spectroscopic Ellipsometry: Principles and Applications, Wiley, 2007, ISBN 978-0-470-01608-4. Excerpt: https://catalogimages.wiley.com/images/db/pdf/9780470016084.excerpt.pdf

    Verified: abstractSupports: Ψ/Δ as the measured amplitude ratio and phase difference; real-time monitoring and process control

  10. [norman1991]B

    S. A. Norman, C. D. Schaper, S. P. Boyd, "Improvement of Temperature Uniformity in Rapid Thermal Processing Systems Using Multivariable Control," 1991. https://web.stanford.edu/~boyd/papers/temperature_uniformity.html

    Verified: abstractSupports: Non-uniformity during ramps causes slip, which limits the ramp rate. This is the slew limit in thermal_setpoint

  11. [uspto6403925]C

    US Patent 6,403,925, "System and method for thermal processing of a semiconductor substrate." https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/6403925

    Verified: abstractSupports: Edge-cool gradients above ~800 °C produce slip lines

  12. [uspto6034356]C

    US Patent 6,034,356, "RTP lamp design for oxidation and annealing." https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/6034356

    Verified: secondarySupports: Typical RTP ramp rates 20–100 °C/s versus 5–10 °C/min in furnaces

Collaborative robotics

  1. [marvel2017]B

    J. A. Marvel, R. Norcross, "Implementing speed and separation monitoring in collaborative robot workcells," Robotics and Computer-Integrated Manufacturing (NIST). https://doi.org/10.1016/j.rcim.2016.08.001 · https://www.nist.gov/node/1097971

    Verified: abstractSupports: ISO/TS 15066 SSM protective separation distance and how to implement it

  2. [szabo2012]B

    S. Szabo, W. Shackleford, R. Norcross, J. Marvel, NIST IR 7851 (2012). https://nvlpubs.nist.gov/nistpubs/ir/2012/NIST.IR.7851.pdf

    Verified: abstractSupports: Laser-scanner SSM testbed that issues stop/restart from the separation distance

  3. [isots15066]A

    ISO/TS 15066, Robots and robotic devices — Collaborative robots. Overview: https://www.automate.org/tech-papers/iso-ts-15066-explained

    Verified: secondarySupports: SSM as one of the four collaborative modes; supplements ISO 10218-1/-2

  4. [iso10218]A

    ISO 10218-1/-2, reduced speed of 250 mm/s. Quoted by https://www.controldesign.com/safety/functional-safety/article/55300304/how-to-understand-safe-reduced-speed-and-safe-limited-speed and https://manual.doosanrobotics.com/en/user-manual/3.2.1/2-a-series/manual-mode

    Verified: secondarySupports: The 250 mm/s reduced-speed cap used in ssm_speed_limit

Control systems

  1. [scilab_aw]D

    "PID Anti-Windup Schemes," Scilab. https://scilab.org/pid-anti-windup-schemes

    Verified: textSupports: Conditional integration and back-calculation are the two basic anti-windup schemes (integrate uses conditional integration)

  2. [astrom_murray]B

    K. J. Åström, R. M. Murray, Feedback Systems, Princeton University Press (PID chapter, integrator windup). Course copy cited by MathWorks: http://www.cds.caltech.edu/~murray/courses/cds101/fa02/caltech/astrom-ch6.pdf

    Verified: secondarySupports: Standard reference for windup

Navigation and autonomy

  1. [nasa_safeguard]B

    NASA Langley, Safeguard geofencing: https://technology.nasa.gov/patent/LAR-TOPS-244 · NTRS report: https://ntrs.nasa.gov/api/citations/20190000716/downloads/20190000716.pdf · geofence algorithms proved in PVS: https://ntrs.nasa.gov/api/citations/20170009617/downloads/20170009617.pdf

    Verified: abstractSupports: Precedent for formally verified stay-in/stay-out geofencing that runs independently of the autopilot

Industrial IoT

  1. [mqtt311]A

    OASIS, MQTT Version 3.1.1, OASIS Standard, 29 Oct 2014. https://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html

    Verified: textSupports: §4.2: "requires an underlying transport that provides an ordered, lossless, stream of bytes"; §4.3.3 [MQTT-4.3.3-2]: until PUBREL the receiver acknowledges re-sent PUBLISHes and "MUST NOT cause duplicate messages to be delivered"; §4.6 [MQTT-4.6.0-1] re-send in original order

  2. [emqx_qos]D

    EMQX, "Introduction to MQTT QoS." https://emqx.io/blog/introduction-to-mqtt-qos

    Verified: abstractSupports: Sender-side QoS 2 flow

  3. [namur_ne43]A

    NAMUR NE 43 (ed. 2021-07-26), standardization of the failure signal level of digital transmitters. https://www.namur.net/en/publications/news-archive/ne-43-has-been-revised.html

    Verified: secondarySupports: 3.8–20.5 mA measurement band; ≤ 3.6 mA or ≥ 21 mA signals a failure. Bands quoted by https://www.microcontrol.net/en/service/measurement-technology/industrial-standard-signals/ and https://www.electricalvolt.com/what-is-namur-ne-43

Manufacturing machinery

  1. [iso13851]A

    ISO 13851:2019, Two-hand control devices. https://committee.iso.org/standard/35560.html

    Verified: secondarySupports: Type III: both actuators within 0.5 s, release before re-triggering. Quoted by Eaton (https://origin.golfpride.com/gb/en-gb/markets/machine-building/service-and-support-machine-building-moem-service-eaton/blogs/Two-hand-control-for-machinery-blog-functional-safety.html) and by Phoenix Contact's type IIIA relay, "synchronous activation monitoring < 0.5 s" (https://www.phoenixcontact.com/us/products/2700571/pdf, tier C)

  2. [iso13855]A

    ISO 13855, positioning of protective equipment: S = K·T + C, K = 2000 mm/s, C = 8(d − 14) for d ≤ 40 mm. Quoted by https://www.issa.int/sites/default/files/documents/prevention/2Light_Curtain_2011_en-36159.pdf and https://www.leuze.com/en-us/navigation/0942f478ebd948d9b0b7c4c7734c3714

    Verified: secondarySupports: light_curtain_distance. Sources disagree on the K = 1600 / 500 mm switch-over between editions, so the model always uses K = 2000 (the larger distance)

Critical process systems

  1. [csb_t2]A

    U.S. Chemical Safety Board, T2 Laboratories explosion (2009). https://www.csb.gov/csb-finds-t2-laboratories-explosion-caused-by-failure-of-cooling-system-resulting-in-runaway-chemical-reaction-report-notes-company-did-not-recognize-hazards-of-chemical-process/

    Verified: abstractSupports: Cooling failure leading to runaway reaction (4 killed, 28 injured nearby). This is the ReactorSis scenario

  2. [lundteigen_sis]B

    M. A. Lundteigen, M. Rausand, SIS book ch. 12, "Spurious trip rate," NTNU. https://ntnu.edu/documents/624876/1277046207/SIS+book+-+chapter+12+-+Spurious+trip+rate/ad91f310-f8b2-41f5-a923-3e9e22971f75

    Verified: abstractSupports: 2oo3 tolerates one fault both against failure to trip and against spurious trips; the two high_temp_trip properties

  3. [iec61511]A

    IEC 61511, Functional safety — SIS for the process industry sector. Hardware fault tolerance by SIL (IEC 61511-1:2018 §11.4), as summarized by https://open-exam-prep.com/study-guides/pe-control-systems/sis-design-sil/sis-design-constraints

    Verified: secondarySupports: Voting architectures and HFT

  4. [kenexis_2oo3]C

    Kenexis, "Comparison of 2oo3 voting and 2oo2 voting." https://kenexis.com/wp-content/uploads/2018/11/Comparison-of-2oo3-voting-and-2oo2-voting.pdf

    Verified: abstractSupports: Cost and complexity trade-offs of 2oo3

Surgical robotics

  1. [rosenberg1993]B

    L. B. Rosenberg, "Virtual fixtures as tools to enhance operator performance in telepresence environments," Proc. SPIE 2057 (1993). https://doi.org/10.1117/12.164901

    Verified: abstractSupports: Origin of virtual fixtures

  2. [abbott2007]B

    J. J. Abbott, P. Marayong, A. M. Okamura, "Haptic Virtual Fixtures for Robot-Assisted Manipulation," Robotics Research, Springer, 2007. https://doi.org/10.1007/978-3-540-48113-3_5 · PDF: https://my.eng.utah.edu/~jabbott/pmwiki/uploads/Main/Abbott_RoboticsResearch07.pdf

    Verified: abstractSupports: Forbidden-region virtual fixtures keep the manipulator out of forbidden regions (fixture_step); da Vinci and the JHU Steady-Hand robot

  3. [iec80601277]A

    IEC 80601-2-77:2019+AMD1:2023, robotically assisted surgical equipment (RASE). https://www.iso.org/standard/68473.html

    Verified: abstractSupports: Basic safety and essential performance of RASE/RASS

Medical devices (infusion pumps)

  1. [fda_ipii]A

    U.S. FDA, White Paper: Infusion Pump Improvement Initiative, April 2010. https://www.fda.gov/medical-devices/infusion-pumps/white-paper-infusion-pump-improvement-initiative · PDF: https://www.fda.gov/media/116949/download

    Verified: abstractSupports: ~56,000 adverse-event reports (2005–2009), 87 recalls (14 Class I); software defects including failures of built-in safety alarms; problems traced to design and engineering

  2. [kim2011gpca]B

    B. Kim et al., "Safety-Assured Development of the GPCA Infusion Pump Software," UPenn. https://repository.upenn.edu/cis_papers/475

    Verified: abstractSupports: FDA Generic PCA reference model checked in UPPAAL against FDA's generic safety requirements

  3. [gpca_umn]B

    University of Minnesota CRISYS, GPCA requirements and artifacts. https://crisys.cs.umn.edu/gpca.shtml

    Verified: abstractSupports: Home of the GPCA requirements documents

Public safety

  1. [mutcd4d26]A

    FHWA MUTCD (2009) §4D.26, Yellow Change and Red Clearance Intervals. Quoted by the NJDOT technical appendix (https://dot.nj.gov/transportation/about/publicat/lmreports/pdf/2013rlrtechnicalappendix.pdf) and a state reprint (https://regulations.justia.com/states/delaware/title-2/2000/2400/2402/part-4/chapter-4d/section-4d-26)

    Verified: secondarySupports: A steady yellow follows every green; yellow should last 3–6 s; red clearance is set by engineering practice. This is the Yellow phase that every green passes through

  2. [mmu]D

    Conflict Monitor Units and Malfunction Management Units (NEMA TS-1/TS-2). https://open-exam-prep.com/study-guides/imsa-traffic-signal-i/cabinet-wiring-and-components/cmu-and-mmu

    Verified: abstractSupports: Hardware monitor that forces flash on conflicting greens. NoConflictingGreens is the same property, proved at design time

  3. [heitmeyer1994]B

    C. Heitmeyer, N. Lynch, "The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems," MIT LCS TM-511 / IEEE RTSS 1994. https://groups.csail.mit.edu/tds/papers/Heitmeyer/TM-511.html · benchmark: https://groups.csail.mit.edu/tds/grc.html

    Verified: abstractSupports: Safety (gate down whenever the crossing is occupied) and utility (gate up otherwise). This is the LevelCrossing model

Cybersecurity

  1. [nist80063b]A

    NIST SP 800-63B, Digital Identity Guidelines: Authentication, §3.2.2 Rate Limiting (Throttling). https://pages.nist.gov/800-63-4/sp800-63b.html

    Verified: textSupports: No more than 100 consecutive failures per authenticator (then disable it); agencies may set lower limits. The model's 5 is such a lower limit

  2. [beurdouche2015]B

    B. Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS," IEEE S&P 2015, pp. 535–552; CACM reprint https://doi.org/10.1145/3023357 · https://hal.archives-ouvertes.fr/hal-01114250

    Verified: abstractSupports: State-machine bugs (SKIP, FREAK) let an attacker skip messages. This is the ClientHandshake seeded bug

  3. [ncc_smack]C

    NCC Group, "SMACK: SKIP-TLS & FREAK SSL/TLS vulnerabilities." https://www.nccgroup.com/research/smack-skip-tls-freak-ssltls-vulnerabilities/

    Verified: abstractSupports: CVE-2014-6593 (SKIP-TLS), CVE-2015-0204 (FREAK)

  4. [rfc2697]A

    J. Heinanen, R. Guerin, RFC 2697, A Single Rate Three Color Marker, 1999. https://www.rfc-editor.org/rfc/rfc2697

    Verified: textSupports: Token buckets that start full and fill at a committed rate, capped at the burst size (refill, spend)

  5. [nist80053ac5]A

    NIST SP 800-53 Rev. 5, AC-5 Separation of Duties. Catalog summary: https://www.upguard.com/compliance/nist-sp-800-53/ac/ac-5

    Verified: abstractSupports: SeparationOfDuties axiom

Automotive

  1. [iso15622]A

    ISO 15622, Adaptive cruise control systems. https://www.iso.org/standard/89465.html

    Verified: abstractSupports: ACC control strategy, minimum functionality, driver interface, failure reaction

  2. [bernsteiner2016]B

    S. Bernsteiner, Integration of Advanced Driver Assistance Systems on Full-Vehicle Level, TU Graz, 2016, ch. 6, p. 78. https://austria-forum.org/web-books/driverassistance00en2017isds/000100

    Verified: textSupports: Minimum selectable time gap of 1 s in one standard and 0.8 s in another; Fancher et al. recommend 1–2 s. The model's 1.5 s lies in that range

Battery systems

  1. [uspto11592485]C

    US 11,592,485 B2, "Methods and apparatus for contactor weld detection in a vehicle." https://patents.google.com/patent/US11592485

    Verified: abstractSupports: Welded main contactor detected when the load-side voltage does not decay after an open command

  2. [uspto12077054]C

    US 12,077,054 B2, "Vehicle main contactor weld detection system." https://patents.google.com/patent/US12077054

    Verified: abstractSupports: Inrush-based weld detection and response

  3. [uspto10476262]C

    US 10,476,262, "Dual-bus battery precharge circuit." https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/10476262

    Verified: abstractSupports: Precharge before main contactor closure; welds come from inrush above making capacity (ClosedOnlyAfterPrecharge)

Aerospace

  1. [airbus_laws]D

    Airbus normal-law protections, as summarized from Airbus FCTM material by Code7700: https://code7700.com/airbus_control_laws.htm · FlyByWire A32NX (simulator) guide: https://docs.flybywiresim.com/pilots-corner/a32nx/a32nx-advanced-guides/protections/overview/ · https://en.wikipedia.org/wiki/Flight_control_modes

    Verified: secondarySupports: Bank beyond 33° needs continuous sidestick input, release returns to 33°, 67° limit; between α-prot and α-max the stick commands AoA, α-max is never exceeded; α-prot disengages the autopilot. Illustrative only: verify against the type's FCOM