Why Buran Had Four Computers, Not Three — and What a Lean Proof Adds

Date: September 24, 2026 · Author: Dmitrii Zatona An-225 carrying Buran, 1989. Photo: Vasiliy Koba, CC BY-SA 4.0 , via Wikimedia Commons ; converted to grayscale, tonally adjusted and cropped. This version: CC BY-SA 4.0. TL;DR Buran’s flight computer was four identical Biser-4 machines running the same programs synchronously. A comparison scheme blocked a failed one, and the design had to survive any two failures (Section 1). Four is what two failures cost if a failed channel is found by comparing outputs alone. It is not the 3f + 1 of Byzantine agreement, which is a different problem (Sections 2 and 3). Copies of one program share its bugs: STS-1, the Boeing 787’s generator controllers, Ariane 501, QF72. The industry answers with dissimilarity and verification together (Section 4). I wrote one step of such a voter in Rust and proved five theorems and two corollaries about it in Lean 4, over the code Aeneas generated from it (Sections 5 and 6). The proof covers the voter, not the flight code: four channels that agree on a wrong command get it through (Sections 4 and 7). The proof tools used here are not DO-330 qualified, and I found no completed public DO-178C or ECSS qualification of a Rust toolchain (Sections 7 and 8). On 15 November 1988 the Soviet orbiter Buran was launched from Baikonur on its first and only flight, a test flight without a crew, and landed in automatic mode. Its onboard computing was a multichannel complex built from Biser-4 computers, designed at NIIAP, the organisation of N. A. Pilyugin that is now NPCAP. Four identical Biser-4 machines flew. Each is one channel of a redundant set, and from here on I call them channels. What sent me into the sources was one description of those four channels: identical machines, synchronous, running the same programs, with a comparison scheme at the output and a requirement to survive any two failures. Voting textbooks start at three channels, and an engineer who hears “four computers” today tends to reach for 3f + 1, the bound from the Byzantine generals papers, because four is exactly 3f + 1 for one fault. For Buran that reading is wrong, and why it is wrong is the most useful part of the story. A disclosure, because the second half of the article is my own work. I write machine-checked proofs about Rust code, for example that it cannot panic, as paid work; cose-parse-nopanic, a COSE envelope parser with its theorems checked in Lean, is one. A voter is small, and every command a redundant system issues passes through it, which made it a good test of the same pipeline. As Section 4 shows, a proof about it also says nothing about a bug the four channels share, and that limit shapes everything after it. Sections 1 to 4 are the history and the theory; Sections 5 to 8 are the voter, its proof, the proof’s limits, and where Rust stands in flight software. 1. What the sources say about Biser-4, Buran’s redundant flight computer The open record on Biser-4 is thin, and its sources do not weigh the same. 1.1 Four sources of unequal weight Most technical detail comes from buran.ru , Vadim Lukashevich’s history site. Its control-system pages describe the computing complex, the comparison scheme and the synchronisation, with a table of characteristics down to word widths and link speeds. They name no author and seem to draw on a 1995 book they do not cite; the book was not checked for this article. V. D. Parondzhanov, whose laboratory at Pilyugin’s organisation was assigned the complete development of Buran’s computing system, left a participant’s account. It is known from a 2011 repost on the RSDN forum ; where it first appeared has not been established. It adds which machines flew and that a program was written for survivability after failures.