Axis Confusion
The kind of thing changes, unacknowledged.
Mars Climate Orbiter — pound-force-seconds read as newton-seconds.
Public analysis · patent-pending library
oAOML
Semantic legality for reality-coupled systems
The engineering projection. oAOML tracks what a value has been through — a real reading or a prediction, your own sensor or a relayed one, live or simulated, fresh or stale — and refuses every state transition that crosses a boundary it should not. Illegal transitions are reported, not permitted.
Correct code that still kills
Therac-25, Knight Capital ($440M in 45 minutes), Ariane 5, the Mars Climate Orbiter — every one passed its tests and did exactly what it was told, yet each crossed a boundary that should never be crossed. The illegality lived in the values’ runtime histories, where no compiler and no units library can see it. The public Engineering Failure Analyses re-reads eighteen such disasters at the level of the individual judgments that failed.
M[A] ↛ A, at runtime
A value that only resembles a measurement — a prediction, a relayed reading, simulator output, a stale fix, a confidence score — must never silently substitute for the real thing. Introducing that mark is free and honest; discharging it, presenting the resemblance as a bona-fide measurement, requires a method the domain has explicitly licensed. Launder simulation into the live pipeline and you get the Knight Capital failure, caught at the transition where it happens. This is oAOML’s projection of the AOML v2.2 schema M[A] ↛ A.
Formally verified
The oAOML-library is implemented in SPARK Ada — no runtime exceptions, memory-safe, certification-grade (DO-178C, ISO 26262). Three layers: a SPARK-proved core, a diagnostic API that returns reasons instead of crashing, and convenient domain kits. Fully-proved exemplars ship for sensors, drone navigation, and trade settlement.
Status
The operational analysis is public and deposited with a DOI. The enforcement library — the oAOML-library — is patent-pending and not yet publicly released; it is the layer Breakwater builds on.
The five faults it blocks
Operator Overextension
An operation applied beyond its valid scope.
Therac-25 — a mode change outran the hardware it commanded.
Habitat Mismatch
The wrong validation method for the context.
Imperial and metric are different validation habitats.
Stratification Collapse
Levels of abstraction mixed.
Ariane 5 — a runtime value forced into a spec constant.
Contrast Frame Collapse
The reference frame that gives meaning is lost.
Knight Capital — test code ran in production.