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

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.

B. N. Vikhorev and A. G. Glazkov of NPCAP wrote abstracts for the XXXI Academic Readings on Cosmonautics in 2007 (archived copy ). This is the developer’s own account. On Biser-4 it says little: that the redundancy was fourfold, and why. The mechanisms it details belong to the predecessors, kept apart below.

V. Kryukov and A. Petrenko of the Keldysh Institute of Applied Mathematics described PROL2, the language created for Buran’s onboard-systems software, in a 1996 paper .

Russian quotations below are translated.

1.2 What is stated, and what is not

The table sets what the sources state beside what none of them states. The second half is not a list of gaps to fill by inference; it is what this article’s model has to supply with rules of its own, each labelled in Section 5.

The stated half is an architecture. The unknown half is the list of questions a designer of a redundancy manager asks first — how a failed channel is identified, what a disagreeing pair does, whether all channels see the same inputs, where four outputs become one command — and every one is open for Biser-4.

1.3 The requirement and the clock

Parondzhanov states what the two-failure requirement was for: under any two failures the control system had to secure “saving the crew’s lives and returning Buran to Earth”. buran.ru states it as a condition on the computing complex, and NPCAP’s abstract ties the fourfold redundancy to it.

Synchronisation was done in hardware. buran.ru explains why: software synchronisation of four machines in real time, under any combination of permitted failures, is “extremely complex and insufficiently reliable”. Parondzhanov draws the contrast directly: “unlike the Americans, who used software synchronisation”, Buran’s four were synchronised in hardware. One clock source fed all eight machines a 4 MHz grid and an interrupt every 32.8 ms, and was itself built as five redundant channels with a three-of-five vote on each output.

Synchronisation matters here because comparing outputs word for word only makes sense if the channels compute the same frame at the same time; a channel a step behind looks exactly like a failed one.

1.4 One program, and where it lived

All four channels ran the same programs; buran.ru and Parondzhanov say so in the same words. buran.ru’s software page adds how they were built and held: a “specialised high-level language” disciplined the integration of separately written programs, and the operating system was designed around functions that included “restoring the computing process after upsets”. The flight software, “hundreds of thousands of words”, lived on an onboard tape recorder, and each zone of the tape was written twice. Kryukov and Petrenko name the onboard-systems language PROL2 and put the software written over four years at “over a million statements”. Parondzhanov adds that PPN, the survivability program, was designed in the DRAKON notation and coded in Biser-4 assembly.

No source mentions a separately written backup program of the kind the Shuttle carried. That is silence, not evidence of absence, and Section 4 explains why it matters most.

1.5 The predecessors: Argon-11S and Biser-2

Vikhorev and Glazkov do describe mechanisms, but for Biser-4’s predecessors, and there they stay. Argon-11S was triplicated, with analogue majority voting of its output commands, and parried upsets by exchanging information between its lanes, the family’s word for channels. Biser-2 had a bitwise majority element at the output of its input/output channel — a data path, not a redundant channel — that recorded an anomaly in any one lane “in addition to” a readiness signal. When it recorded one, an inter-lane exchange copied RAM into the affected lane “in one computer cycle”. Those exchanges served recovery from upsets, not agreement on inputs, and the same authors note that upsets are at least an order of magnitude more frequent than failures.

It is tempting to carry both mechanisms over to Biser-4. The numbers resist the second: a full copy of Biser-4’s 131,072-word RAM over a link of 61,440 words per second, one RAM word per link word, would take about 2.1 seconds, some 65 of its 32.8 ms cycles. That is this article’s arithmetic from the buran.ru table, not a statement from any source, and whether Biser-4 restored a smaller state over the link is not said. The first, a bitwise majority element that identifies the failed lane, is stated nowhere for Biser-4.

2. Four channels, two failures: why not triple modular redundancy

The short answer is arithmetic. The long one is that the arithmetic holds only under an assumption the sources do not confirm, and that the Space Shuttle counted the same four computers differently.

2.1 Masking and disconnecting

Triple modular redundancy masks one fault by majority vote over three channels: the wrong output of one channel never reaches the actuator, because two correct channels outvote it. The arithmetic is 2f + 1, because the correct channels must outnumber f faulty ones at the same moment. Buran’s clock source used exactly that: five channels with three-of-five votes mask two simultaneous faults, 2f + 1 for f = 2 (this article’s arithmetic).

Buran’s computers were rated differently. They were to keep working after any two failures, by comparing outputs and blocking a failed channel. That is detection and isolation, not masking: faults are handled one after another, and each costs a channel.

2.2 The count, if comparison is all there is

How the failed channel was identified, the sources do not say. Take the simplest reading: by comparison of outputs alone. With three channels, the first failure is a 2–1 split, the odd channel is blocked, and two remain. The second failure is a 1–1 split between the survivors, and a comparison cannot tell which of the two is wrong. Three channels give one failure survived and a second one detected.

With four, the first failure is 3–1 and the odd channel goes; the second is 2–1 among the remaining three, and it goes too. A pair is left that still agrees. On that reading, two failures handled one after the other need four channels, which fits Buran’s four; NPCAP’s abstract ties the fourfold redundancy to the two-failure requirement.

The diagram’s identification rule is this article’s model, not a sourced mechanism. The last arrow is the open one: no source describes what happens when the remaining pair disagrees. Parondzhanov writes that a program, PPN, was provided for managing survivability when one, two or three machines failed; so Buran’s designers planned for more than the pair, but what PPN did is not on the record.

2.3 The reading the argument rests on

The count in 2.2 carries the whole “why four” argument, and it rests on one assumption: that a failed channel can only be found by comparison. A channel that detects its own failure does not need to be outvoted, and with self-detection fewer channels could cover two failures.

The family had a second indicator of exactly that kind. Biser-2’s majority element, per Vikhorev and Glazkov, worked “in addition to” a readiness signal. Whether Biser-4 had one, the sources do not say. So the honest statement is conditional: if comparison was all Biser-4 had, four channels were the minimum for two failures; if it had self-detection, the four bought something else.

2.4 How the Shuttle counted the same four

The Space Shuttle is the obvious comparison, and it counted the same arithmetic differently. J. E. Tomayko’s NASA history (CR-182505, chapter 4 ) explains the Shuttle’s early requirement, fail operational / fail operational / fail safe, by majority: it needed five computers, so that after two failures three would remain to avoid “the feared standoff possible in dual computer systems (one is wrong, but which?)”. NASA then relaxed the requirement to fail operational / fail safe, which “allowed the number of computers to be reduced to four”. In that accounting a level is fail-operational only while a voting majority remains. By that counting, four channels identified by comparison alone give fail operational / fail safe.

Buran’s sources state the same four channels differently: after two failures the system continues to work on two. How that pair was kept operational is not described.

The Shuttle is also a foil for where the vote happened. Tomayko notes that such close synchronisation between computers “had not been done before”, and the vote itself happened at the actuators, where “the failed computer’s commands are physically out-voted”. And the Shuttle deliberately did not switch a failed computer off automatically; the crew had to cut its power. Tomayko gives the reason in one sentence: “This prevents a generic software failure causing all the computers to be automatically shut off.” Buran’s scheme, as described, blocked a failed output by itself. The Shuttle’s designers had a failure in mind that a comparison of identical programs cannot see, and Section 4 is about it.

2.5 The standard answer to the standoff

The standoff has a standard industrial answer, which the Buran sources neither confirm nor exclude: channels that check themselves. Each Airbus A320-to-A340 flight control computer (Avionics Handbook, ch. 12 ) is a control channel watched by a monitor channel; on disagreement between the two “the computer affected by the failure is passivated”, and the computer with the next priority takes over. NASA’s Orion feeds its four flight computers to a source selector that picks one by priority, not by majority. As reported by Aviation Week, SpaceX’s Dragon has “three computer units, each of which have two computers checking on each other”.

In each case each member of a pair can say whether it is the one that failed — the capability 2.3 found unrecorded for Biser-4.

3. Output voting is not Byzantine agreement

Four is 3f + 1 for f = 1, the minimum for Byzantine agreement with one traitor. Buran is not an instance of it, and the relation between the two problems is exactly where its sources go silent.

3.1 The agreement problem

The bound comes from Pease, Shostak and Lamport (1980 ) and Lamport, Shostak and Pease (1982 ). One commander sends a value; the commander or some receivers may be faulty and send different values to different receivers; every correct receiver must end with the same value, and with the commander’s value if the commander is correct. With unsigned messages the problem is “solvable for, and only for, n ≥ 3m + 1”, where m is the number of faulty processors. At four processors and one fault, the algorithm OM(1) takes two rounds: the commander sends, each lieutenant relays what it received to the other two, and each takes the majority. With unforgeable signatures the bound goes away; the 1982 paper says outright that “our previous argument that four generals are required … no longer holds”.

The problem came from practice: Lamport notes it “was formulated by people working on SIFT”, a fault-tolerant aircraft-control computer then under development at SRI.

3.2 Where voting meets agreement

Output voting is a different problem, and the 1982 paper’s section “Reliable Systems” says where the two meet. Majority voting over replicated processors is “based upon the assumption that all the nonfaulty processors will produce the same output”. That holds only if they started from the same input. With a single input source, “a malfunctioning component can give different values to different processors”, and wiring the source to every processor does not help, because a marginal signal on a wire can be “interpreted by some processors as a 0 and by others as a 1”. The authors’ conclusion is that identical inputs can only be guaranteed by solving the Byzantine generals problem among the processors. Output voting masks f faults with 2f + 1 channels only after the input problem has been solved.

Agreement, like comparison, sits on synchronisation: detecting a missing message needs timeouts, and those need “clocks that are synchronized to within some fixed maximum error”.

3.3 How many faults four nodes survive

Thambidurai and Park’s hybrid fault model, as reworked by Lincoln and Rushby (FTCS-23, 1993 ), counts by kind of fault. It separates arbitrary (a), symmetric (s) and manifest (c) faults — a manifest fault being one the receivers can all detect — and their algorithm OMH(m) needs “more than 2(a + s) + c + m processors and m ≥ a”. At n = 4 and m = 1, which is this article’s arithmetic and not a case the paper gives, four nodes survive one arbitrary fault, or one symmetric, or two manifest; with only manifest faults present, the paper’s Theorem 2 allows up to three. Four nodes cope with two faults at once only if both announce themselves.

The 777 primary flight computer met the same wall: Y. C. Yeh writes that a rigorous proof of algorithms against the Byzantine generals problem “is not possible for any triple redundant system”, and Boeing addressed it through data-bus requirements.

3.4 Byzantine faults in real hardware

Byzantine faults are physical. Driscoll, Hall, Sivencrona and Zumsteg (SAFECOMP 2003) describe a signal stuck at ½, between a valid 0 and 1, and a “Schrödinger’s CRC”, where receivers with different thresholds read different data and “each copy has a correct CRC for its data”. They report a TTP/C cluster splitting into cliques under heavy-ion radiation, and Honeywell’s MMFCS prototype, where Byzantine failures recurred on average every 50 seconds, one control cycle in a thousand at 20 Hz. Such faults, they write, “propagate through traditional fault containment zones”. Their verdict: “The Byzantine Generals Problem is not a myth.”

The Shuttle supplied a case. On 13 May 2008, during fuel loading for STS-124, “a 3-1 split of its four control computers occurred”, which became 2-1-1 and then 1-1-1-1, and “none of the computers or their intercommunications were faulty!” The single fault was a cracked diode in the bus interface of one multiplexer-demultiplexer, MDM FA2, the box that sends messages to the four computers. The account is from slides by K. Driscoll of Honeywell, posted on a NASA server; they are not an official NASA finding, and no separate NASA report on the event was found.

3.5 What that leaves for a model of Buran

So there are two problems, and Buran’s sources describe one of them: output voting over four channels. How the channels came to hold identical inputs they do not say — whether each read the sensors directly, or whether the inter-channel link ever carried input values. The documented uses of inter-lane exchange in the predecessors, Argon-11S and Biser-2, were recovery from upsets. A model built from the description has to assume that correct channels saw the same input, and Section 6 states that assumption as an explicit premise, hAgree.

4. One program on four machines: common-mode software failure

Four machines running one program on one input make the same mistake at the same moment, and the comparison sees four agreeing outputs. Redundancy of this kind cannot mask a fault every copy shares, by construction. The cases fall into two groups.

4.1 Identical units running identical software

STS-1, first launch attempt, 1981. About twenty minutes before launch, the Shuttle’s backup flight system could not synchronise with the four primary computers. The cause, per NASA , was “a minor programming error that had survived thousands of hours of testing”, which made the four primary computers begin processing 40 milliseconds earlier than they should. Engineers later estimated that the problem “would have occurred on just one out of every 67 launches”. The four identical computers agreed with each other and could not reveal it. It surfaced at the interface to the separately written backup.

Boeing 787, 2015. Four identical controllers, one per generator, not a voted set, which makes the point sharper. Per FAA Airworthiness Directive 2015-09-07 , a software counter in each “will overflow after 248 days” of continuous power. “If the four main GCUs … were powered up at the same time”, then “all four GCUs will go into failsafe mode at the same time”, and the aircraft loses all AC power, whatever the flight phase. It was found in laboratory testing, not in flight.

Orion, a design threat rather than an event. NASA’s presentation on Orion’s backup flight software  names the case its four flight computers, feeding a source selector by priority, are designed against: “If all four computers fail simultaneously due to a latent software bug”, a dissimilar backup takes over.

4.2 Other layouts that failed the same way

Two further cases confirm the point, though neither is a four-channel analogue.

Ariane 501, 4 June 1996. Two inertial reference units ran in parallel, one active and one in hot standby. At H0 + 36.7 seconds the standby failed, and about 0.05 seconds later the active one, “identical to the back-up system in hardware and software, failed for the same reason”: an unprotected conversion of a 64-bit floating-point value to a 16-bit signed integer. The Inquiry Board  calls it “not due to random failure but a design error”. Part of the error sat in the requirements, where the parties had “jointly agreed not to include the Ariane 5 trajectory data”. The Board traced the shutdown design to a “culture within the Ariane programme of only addressing random hardware failures”.

Qantas 72, Airbus A330, 7 October 2008. “Each FCPC was loaded with identical, uncorrupted operational software.” One of three air data units produced angle-of-attack spikes, and the flight control computers’ algorithm could not handle “multiple spikes in AOA from one ADIRU that were 1.2 seconds apart”. The aircraft pitched down, injuring at least 110 of 303 passengers and 9 of 12 crew. Of reviews, analysis, tests and simulation, the ATSB  writes: “None of these activities identified the design limitation”.

4.3 Dissimilarity, and what it does not replace

The industry answers with two things at once. The first is dissimilarity. The Shuttle’s backup software was written by another contractor “in the interest of avoiding a generic software failure”. Airbus required on the A320 that “the five computers all be of different natures to avoid common mode failures”: in practice two types of computer, ELAC and SEC, from different teams on different processors, each a control/monitor pair with its own software. The 777 primary flight computer uses “three different Ada compilers” and three different processors, from common source. Yeh’s paper gives the reason in general form: “Design errors can defeat redundancy strategies”.

Identical hardware fails together too. Airbus’s account of its fly-by-wire experience (ICAS 2006 ) reports an A320 flight that lost both ELACs to overheating, through a batch component out of its specified temperature range, and an A340 flight where “a very peculiar hardware failure of a single component” temporarily trapped all three primary computers.

The second answer is verification, and the builders of dissimilar systems say plainly that the first does not replace it. At Airbus, “Dissimilarity is an additional precaution”, “not used to reduce the required software quality effort”; for the 777, dissimilarity “will not be an alternate to the rigorous verification and validation”. Machine-checked proof enters that second line through DO-333, the formal methods supplement to DO-178C. Per NASA’s case-study report (NASA/CR-2014-218244 ) and D. Cofer’s papers — the standard itself was not read for this article — it “generally allows the testing described above to be replaced by a comparable formal analysis”, and “some on-target testing is still required”. The report adds two conditions: evidence that the proved properties are preserved in the object code, and qualification of the proof tools under DO-330, at TQL-4 for levels A and B. At Airbus, “Since 2002, a formal approach to Unit Verification is also used industrially” (Souyris and colleagues).

For Buran, the sources establish identical programs on all four machines and do not mention a dissimilar backup program.

4.4 Where the proof in this article stops

Sections 5 and 6 prove properties of the voter, not of the flight code that feeds it. If all four channels agree on a wrong command because the flight program has a bug they share, the proved voter outputs that command; the masking theorem in Section 6 guarantees exactly that. The proof rules out errors in the voter’s implementation relative to its specification. Against a common error in the flight code, what works is proof about the flight code itself: that it does not panic, that it parses its inputs correctly, that the control laws keep their invariants. The voter demonstrates the method on a small piece every command passes through; it is not an answer to common-mode failure.

5. The voter in Rust

A program needs decisions the sources do not make. I call my model a voter; Buran’s hardware was a comparison scheme, and the two words stay apart in what follows. Given which channels are active and each channel’s command word, one step returns a command or none, which channel to switch off, and the active set to continue with.

5.1 The rules, and where each comes from

The rules below are quoted from the repository’s README, each with its label and the reason for it.

• Four channels, synchronous, same programs, output comparison, blocks a failed one, 4 → 3 → 2, two-failure requirement —source . buran.ru states all of it; Parondzhanov corroborates synchronous operation on the same programs; Vikhorev–Glazkov confirm only that the four machines serve the two-failure requirement.
• A blocked channel never returns —ours . The model covers permanent failures, not upsets with recovery as in Biser-2.
• Command word type u64 —ours . Source command words are 36 bits;u64 is the smallest built-in type that holds them, and words are only compared for equality.
• Comparison is whole-word, not bitwise —ours . Biser-2 voted bitwise; at four channels that produces 2–2 ties on single bits.
• Exactly one disagreeing channel among an agreeing majority → majority wins, disagreeing channel disabled —ours . buran.ru says only that the failed output is blocked; this is a reconstruction, not a documented mechanism.
• Two active channels, disagreeing → Undetermined —ours . No source describes the pair.
• Any other disagreement pattern (2–2, 2–1–1, all different at three active) → OutsideHypothesis, no command chosen —ours . A result of the model; Biser-4 has no such state on record.
• One active channel → Agreed, that channel’s own word as the command, unchanged andZero active channels → NoActiveChannels, no command —ours . Neither is reachable from four active channels; both exist so thatstep is total, and no theorem beyond T1 covers them.

Two further readings go with the list. OutsideHypothesis switches nobody off, and the words of channels already switched off are ignored. “No command” is the model’s way of refusing to choose; whether an output stage then holds the last command, blanks the output or hands over to a backup is a flight-safety decision outside the model.

The model stops at the pair. Parondzhanov writes that PPN was provided for a third failure as well; this model has no third-failure behaviour at all, and there it diverges from Buran.

5.2 Three simplifications

Three deliberate simplifications are the ones a redundancy engineer will look for first.

The model is one voter that sees all four words at once. The source puts a comparison scheme at every machine’s output. Replicated comparators must all see the same four words, or they will disagree about whom to block; that is the input problem of Section 3 again, on the output side.

There is no persistence filter. One mismatched frame disables a channel for good, so a single upset in a healthy channel spends one of the two tolerated failures, and by Vikhorev and Glazkov upsets are the more frequent event. Debouncing a miscompare over several frames, or recovering a lane as Biser-2 did, would avoid that. Neither is modelled.

And the channels do not check themselves: there is no readiness signal and no monitor channel, only comparison, the reading of Section 2.2.

5.3 The code

The first version was a chain of if / else if with &&-combined conditions, a direct transcription of the rules. It passed cargo test, but Charon wrote ≈662 MB of LLBC for it; in a reproduction at the same pins, 99.88% of that was step’s translated body. The same truth table as a match on named booleans is 526,561 bytes (≈526.6 KB). Why the ladder exploded I do not know; the measurements are in EXTRACT.md . The four-channel case, copied from rust/src/lib.rs:

/// Resolves a step in which all four channels are active.
///
/// Implementation note: same reasoning as [`triple_step`] — the six
/// pairwise comparisons are named booleans, dispatched with a `match`
/// instead of an `&&`-chained `if`/`else if` ladder.
fn quad_step(words: [Word; 4], active: ActiveSet) -> StepResult {
    let w0 = words[0];
    let w1 = words[1];
    let w2 = words[2];
    let w3 = words[3];
    let eq01 = w0 == w1;
    let eq02 = w0 == w2;
    let eq03 = w0 == w3;
    let eq12 = w1 == w2;
    let eq13 = w1 == w3;
    let eq23 = w2 == w3;
    match (eq01, eq02, eq03, eq12, eq13, eq23) {
        // w0 == w1 == w2 == w3 (eq12/eq13/eq23 follow from eq01/eq02/eq03
        // by transitivity, so they are not tested here).
        (true, true, true, _, _, _) => StepResult::Agreed {
            command: w0,
            active,
        },
        // {0,1,2} agree on w0; channel 3 differs.
        (true, true, false, _, _, _) => StepResult::Majority {
            command: w0,
            disabled: 3,
            active: disable(active, 3),
        },
        // {0,1,3} agree on w0; channel 2 differs.
        (true, false, true, _, _, _) => StepResult::Majority {
            command: w0,
            disabled: 2,
            active: disable(active, 2),
        },
        // {0,2,3} agree on w0; channel 1 differs.
        (false, true, true, _, _, _) => StepResult::Majority {
            command: w0,
            disabled: 1,
            active: disable(active, 1),
        },
        // {1,2,3} agree on w1, w0 differs from all three of them.
        (false, false, false, true, true, true) => StepResult::Majority {
            command: w1,
            disabled: 0,
            active: disable(active, 0),
        },
        // Every other combination: a 2-2 split, a 2-1-1 split, all four
        // different, or (for the six-flag tuple) a combination that real
        // `==` can never actually produce. All fall through to the same
        // no-command result.
        _ => StepResult::OutsideHypothesis { active },
    }
}

The first four arms test only eq01, eq02 and eq03, because equality is transitive. The last arm catches 2–2, 2–1–1 and all-different splits, together with flag combinations that real equality cannot produce, and returns OutsideHypothesis with the active set unchanged. Delete it and the compiler rejects a non-exhaustive match; replace it with a tie-break and you have invented a Biser-4 behaviour. The crate is #![no_std] and #![forbid(unsafe_code)]. The code Charon extracts for the proof, step and the functions it calls, contains no loop, recursion or allocation, so step is a finite decision tree over four fixed slots; the test-only code, which has loops, is outside the extraction.

5.4 Tests

The tests compare step with an independently written oracle that counts how often each value occurs among the active channels instead of branching, over all 16 active sets and every assignment of four words from a three-value alphabet: 1,296 cases. Three symbols cannot make four different words, so that pattern is covered by a separate unit test and by the proof. The only bug the tests found was in the oracle: its three-channel case called three different words a Majority. The test caught the test.

6. The proof in Lean 4, through Aeneas

6.1 From Rust to Lean

The pipeline is the one cose-parse-nopanic uses. Charon  extracts the crate’s MIR, the compiler’s mid-level intermediate form, into LLBC. Aeneas  translates LLBC into a pure functional model in Lean 4, where each function returns ok with a value, fail with an error covering panic, integer overflow and out-of-bounds indexing, or div for non-termination. A theorem that a function returns ok on every input therefore rules all of them out at once. Aeneas handles “a subset of safe Rust”, and the crate forbids unsafe code. The generated Lean is committed unedited, and every theorem is stated over it, not over a model I wrote by hand. Pins: Charon 909ff09a, Aeneas c2015b86, Lean 4.31.0.

6.2 What F and h mean

A is the set of active channels, and out[i] is channel i’s word on a step. T3a and T3b fix a set F of at most two faulty channels: channels with a fault of their own, in hardware or anything else that makes that channel’s word differ from what the fault-free channels produce (one upset is enough). They assume that on every step the channels not in F, the correct ones, agree on a value h, which takes for granted identical inputs and synchronised, deterministic execution. h is what the fault-free channels produce, not necessarily the right command: if the flight code they share has a bug, h is wrong, every premise still holds, and the theorems deliver h.

6.3 One step: T1 and T2

T1, no panic:

For any active set and any command words, step returns ok.

ok includes Undetermined and OutsideHypothesis: this is “no panic”, not “always a command”.

T2, masking in one step, for any active set:

Let |A| ≥ 3, v a value, D = {i ∈ A | out[i] ≠ v}, |D| ≤ 1. If D = ∅, the output is v and A is unchanged. If D = {d}, the output is v, the new A is A \ {d}, and no other channel is disabled.

T2 is the masking theorem Section 4 referred to. It holds for any value v, including a wrong one that every channel agrees on.

6.4 Traces: T3a and its corollaries

T3a, reachable traces, no assumption about the order of failures:

On any finite trace from A = {0,1,2,3}, the invariant “A \ F is nonempty and every disabled channel ∈ F” is preserved by the step, then by induction on the trace. Hence a correct channel is never disabled.

T3a is false for an arbitrary starting state. The counterexample: three active channels, one correct and two faulty that agree on the same wrong value; the correct channel is the lone dissenter and is switched off. So T3a is stated only for traces that start with all four channels active, which activeSeq encodes by starting from allActive. Its two named corollaries follow it:

def allActive : Array Bool 4#usize := Array.repeat 4#usize true
 
def activeSeq (wordsSeq : Nat → Array U64 4#usize) : Nat → Array Bool 4#usize
  | 0 => allActive
  | n + 1 => stepActive (activeSeq wordsSeq n) (wordsSeq n)
 
theorem T3a (wordsSeq : Nat → Array U64 4#usize) (F : Finset (Fin 4)) (hF : F.card ≤ 2)
    (hAgree : ∀ n : Nat, ∃ h : U64,
      ∀ i : Fin 4, i ∈ A (activeSeq wordsSeq n) → i ∉ F → out (wordsSeq n) i = h) :
    ∀ n : Nat, Finset.univ \ A (activeSeq wordsSeq n) ⊆ F
 
theorem T3a_correct_never_disabled (wordsSeq : Nat → Array U64 4#usize)
    (F : Finset (Fin 4)) (hF : F.card ≤ 2)
    (hAgree : ∀ n : Nat, ∃ h : U64,
      ∀ i : Fin 4, i ∈ A (activeSeq wordsSeq n) → i ∉ F → out (wordsSeq n) i = h) :
    ∀ (n : Nat) (i : Fin 4), i ∉ F → i ∈ A (activeSeq wordsSeq n)
 
theorem T3a_nonempty (wordsSeq : Nat → Array U64 4#usize)
    (F : Finset (Fin 4)) (hF : F.card ≤ 2)
    (hAgree : ∀ n : Nat, ∃ h : U64,
      ∀ i : Fin 4, i ∈ A (activeSeq wordsSeq n) → i ∉ F → out (wordsSeq n) i = h) :
    ∀ n : Nat, (A (activeSeq wordsSeq n) \ F).Nonempty

T3a itself proves the “every disabled channel ∈ F” half of the invariant, as univ \ A ⊆ F. T3a_correct_never_disabled states that every channel not in F stays in A on every step. The “A \ F nonempty” half is T3a_nonempty, a proved corollary: every correct channel is active, and F.card ≤ 2 < 4 leaves at least one.

The premise hAgree is needed even from four active channels. Without it, three channels that agree by coincidence switch off a correct fourth, and nothing in step looks at F.

T3a proves that a correct channel is never disabled; it does not prove that a command is issued when two channels fail with wrong values on the same step (a 2–2 split at four active channels gives OutsideHypothesis, no command). “Survives two failures” in this article means only T3b, with its own assumption.

6.5 One fault at a time: T3b

T3b, under my assumption that faults reveal themselves one at a time (no near-coincident faults; latent faults that surface together break it), is:

Additionally, on every step, |{i ∈ A ∩ F | out[i] ≠ h}| ≤ 1. Then: (b) while |A| ≥ 3, the output is h; (c) OutsideHypothesis never occurs; (d) when |A| = 2, both active channels are correct (T3a) and the output is h.

In Lean the statement is one fact per step: for every n and every h satisfying both premises, step returns ok r with resultCommand r = some h and r ≠ OutsideHypothesis. That ties the output to the correct channels’ value. Item (d)‘s “both active channels are correct” is derived inside the proof from T3a; there is no separate theorem for it. Without the assumption, two faulty channels disagreeing with h on the same step give a 2–2 or 2–1–1 split among four active channels, and the result is OutsideHypothesis, with no command.

That rule is more conservative than the hypotheses need. By my reasoning, not by a theorem: under T3a’s hypotheses the correct channels form a block of at least two equal words, so in a 2–1–1 split the agreeing pair is necessarily h, and a plurality rule would lose nothing there. I did not model or prove a plurality variant. The split no rule can resolve is 2–2.

6.6 The pair: T4

T4, the pair:

At |A| = 2 with a disagreement, the result is Undetermined: no command is produced, A is unchanged.

theorem T4 (active : Array Bool 4#usize) (words : Array U64 4#usize)
    (i j : Fin 4) (hij : i ≠ j) (hA : A active = {i, j})
    (hdisagree : out words i ≠ out words j) :
    step active words = ok (StepResult.Undetermined active)

T4 is the model’s answer to the question the sources leave open, and deliberately no answer.

6.7 Axioms and CI

All seven named theorems — T1, T2, T3a, T3a_correct_never_disabled, T3a_nonempty, T3b and T4 — depend only on the axioms propext, Classical.choice and Quot.sound. The project’s Lean files (lean/*.lean) contain no sorry, admit or axiom after comments are stripped, and CI audits the axiom sets of the seven named theorems. CI runs sha256sum -c reports/PROOF.sha256, which binds the committed LLBC and generated Lean to the Rust source and the handwritten proof files, runs cargo test, builds the Lean project, checks those axiom sets, and runs scripts/check-no-sorry.sh. Neither CI job runs Charon or re-extracts LLBC or generated Lean; freshness of the extraction is checked locally with scripts/check-extraction.sh before every commit that touches rust/src/lib.rs.

6.8 What a proof adds over a test

What does Lean add for a function this small? For one call of step, little: it depends only on the active set and on which words are equal, so by my reasoning a four-symbol exhaustive test would cover it. T3a and T3b hold for traces of any length, with their premises written down, where a test stops at some depth. And the method, not this function, is what scales.

Voting logic also has a record of hand proofs that did not hold. In 1993 Lincoln and Rushby, verifying agreement algorithms in PVS, found that for one by Thambidurai and Park, “despite a published proof of correctness, their algorithm is flawed”. Machine-checked work on agreement and voting is not new either. Bevier and Young checked OM(1) and its hardware implementation in the Boyer–Moore prover in 1990; lean-dag proves a DAG consensus protocol at n ≥ 3f + 1 in Lean 4; and a 2025 FSTTCS paper (LIPIcs; arXiv version ) builds a correct-by-construction input-selection voter in Rocq. I did not find a Lean 4 formalisation of a four-channel voter.

7. What this does not prove

• Specification errors. The theorems relatestep to its own definition. Ariane 501 failed partly on requirements, and QF72’s limitation sat in an algorithm over three redundant air-data sources; a proof against either specification would have proved the flaw in.
• Input agreement, or a Byzantine source. Whether the channels could physically have received a step’s words is outside the model. STS-124 is what that gap looks like: with a Byzantine input, the provedstep would switch off a healthy channel on the first 3–1 split, exactly as specified.
• Replicated comparators. Every theorem is about onestep function that sees one array of four words per cycle. That comparators at different channels see the same words, and so block the same channel, is not modelled.
• Synchronisation, timing, the shared oscillator. Not modelled;step is a pure function of one cycle.
• Compilation and the comparison hardware. The proof is about the code Aeneas translated, not a compiled binary; nothing here shows that the properties survive compilation, which DO-333 credit requires. Latent faults in a comparator are outside the model.
• A common error in the flight code. If all four channels agree on a wrong command, the proved voter outputs it. That is what T2 says.
• Transient filtering and reintegration. One mismatched frame disables a channel for good. Biser-2 recovered a lane by copying RAM, and buran.ru lists restoring the computation after upsets among the functions Buran’s operating system was designed around; neither is modelled.
• Behaviour after a third failure. Per Parondzhanov, Buran’s PPN was provided for it; this model stops at the pair.
• Faults outside the hypothesis. Two faulty channels disagreeing withh on the same step, with four channels active, giveOutsideHypothesis : a proved result, not a proved command.
• What to do with a disagreeing pair. T4 proves onlyUndetermined . For Buran the sources are silent; the industrial answer is self-checking channels or a dissimilar backup, and the model has neither.
• Correspondence with Buran. This is a Rust model of a published description, not of Buran’s hardware and assembly.
• The tools. The proof is as trustworthy as the Lean kernel, Charon, Aeneas and the rustc front end that produced the MIR. None of them is qualified under DO-330; Charon describes itself as “beta software”, and the chain has had a soundness bug, since fixed.

8. Rust in flight software today

Qualified Rust compilers exist, outside aerospace. Ferrocene is TÜV SÜD-qualified for ISO 26262 ASIL D, IEC 61508 SIL 3 and IEC 62304 Class C, and for aviation, in its own words , “supports customer certification efforts toward” DO-178C DAL C. AdaCore describes GNAT Pro for Rust as “preparing the toolchain to be used in regulated environments such as DO-178” and says it “offers toolchain qualification and runtime certification”. DLR wrote in 2025 that “there is currently no qualification to a relevant aerospace standard such as DO-178C or ECSS”, and I found no public record of a completed one since.

The rest is studies and demonstrators. ESA has funded evaluations of Rust for onboard software, by N7 Space, Airbus Defence and Space, and DLR. The sat-rs library from the University of Stuttgart flew as an experiment on ESA’s OPS-SAT in 2024. At NASA, a Goddard research project in 2020–2021 took Rust support in the core Flight System from technology readiness level 2 to 4. A 2024 White House report put it in one line: Rust “has not yet been proven in space systems”.

In defence the signal is DARPA’s PROVERS programme, where a Collins Aerospace-led team generates Rust components for the seL4 microkernel and checks their contracts in Verus: “HAMR is being used to develop an experimental version of the mission computer” for expendable drones. Aeneas itself has an industrial user in Microsoft’s SymCrypt, where a “237 KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7 KLOC of Rust”. No public use of Aeneas in avionics or space was found.

What stayed with me from this work is how little of it was proof. Most of it was the rule list in Section 5: deciding, rule by rule, what came from a source and what I was supplying. The theorems are only as honest as that list. The code, the Lean and the reports on what is and is not proved are at github.com/dzatona/quad-voter-proof ; the pinned commands to replay them are on the verification page. More write-ups are on the engineering blog.

If one Rust component of your system must not panic or return a result its specification forbids, a machine-checked proof of that property is contract work I take on.