Why Buran Had Four Computers, Not Three
12 hours ago
- Buran's flight computer used four identical Biser-4 machines running the same programs synchronously, with output comparison to block a failed channel and a requirement to survive any two failures.
- Four channels are needed if only output comparison is available: three channels can handle one failure but fail on the second due to a 1-1 standoff; four channels allow sequential isolation of two failures.
- The Buran design is not an instance of Byzantine agreement (which would require 3f+1 nodes), because it addresses output voting rather than ensuring consistent input agreement across potentially faulty nodes.
- Identical programs on all channels cannot detect common-mode software failures; historical cases like STS-1, Boeing 787 generator controllers, Ariane 501, and Qantas 72 illustrate this limitation.
- The author created a Rust model of a four-channel voter and proved five theorems and two corollaries in Lean 4 using the Aeneas extraction pipeline, covering properties such as panic-freedom, correct masking of up to two sequential faults, and behavior at the pair stage.
- The proofs apply only to the voter implementation, not to the flight code; a common bug in the flight program that all channels share would still pass through the voter without detection.
- The toolchain (Charon, Aeneas, Lean) is not qualified under DO-330, and no public record of a completed DO-178C or ECSS qualification of a Rust toolchain for flight software was found.