Why Buran Had Four Computers, Not Three

Buran’s onboard computing consisted of four identical Biser-4 channels running the same programs in lockstep under a hardware clock, with an output comparison scheme that could block a deviating channel and was required to tolerate any two failures. Open technical sources are limited and uneven: some describe synchronization, word widths, and a two-failure survivability requirement; others note an onboard tape for software and a post-failure survivability program (PPN) without detailing how a failed channel was identified, how a final command was selected, or whether inputs were replicated to all channels. Predecessor systems used triplication and bitwise majority elements, but Biser-4’s explicit design choices and many operational details remain undocumented.

The core argument explains why four channels were used: when failures are detected solely by comparing outputs, surviving two failures requires four channels, which is a different problem than Byzantine agreement (so 3f+1 does not apply here). Running identical software across channels risks common-mode failures - multiple channels agreeing on the same erroneous command - so industry practice combines dissimilarity and verification to mitigate that. To explore the redundancy manager, the author implemented a voter in Rust and produced machine-checked proofs in Lean 4 about its properties; those proofs cover the voter logic only, not the flight code, and chosen toolchains lack public DO-330 qualification, leaving verification limits explicit.