PlaneOS
A trustless execution gate in pure Rust. It isolates the flight surfaces from pilot and autopilot error by proving, on every 500-microsecond control cycle, that the requested manoeuvre cannot violate a lethal aerodynamic invariant.
01 — the problemWhy voting fails
Commercial airliners fly on voting schemes: two out of three flight control computers must agree before a surface moves. When sensors ice over, or a software edge case appears, voting algorithms can agree on a catastrophic manoeuvre — agreement is not correctness, and three computers running the same faulty model will agree with each other.
PlaneOS replaces heuristic agreement with formal satisfiability. A command does not reach a flight surface unless its safety has been proven in advance.
02 — the gateUNSAT opens, SAT clamps
The execution gate sits directly between the flight control computers and the hydraulic and electric surface servos. When a pitch-up is commanded, the gate translates the resulting trajectory into a hazard formula and asks the solver one question: can this command lead to a stall, an overspeed, or a terrain collision within horizon H?
If the answer is UNSAT — the hazard is physically impossible — the gate opens and the actuator deflects. If the hazard is SAT, an excursion is reachable, and the command is clamped to the nearest verified-safe alternative. The pilot keeps authority over everything that is provably survivable; nothing else reaches the surface.
git clone https://github.com/KELLERBABG/PlaneOS.git cd PlaneOS && cargo test # the reproducible verification suite