A four-channel command-word voter’s step shown to mask a disagreeing channel and, on traces from four active channels under a per-step agreement hypothesis, never disable a correct one. 7 theorems, machine-checked.

quad-voter-proof@b2cdeeb · transcript · PROOF.md · Lean CI · CI run

Machine-checked proof of a step of a four-channel command-word comparison scheme, consistent with the open-source description of “Biser-4” (NIIAP): four machines running the same program, synchronously, with an output comparison scheme that blocks a channel that has failed, rated for two failures (degradation 4 → 3 → 2). Hashes, tests, Charon, Aeneas, Lean. 7 theorems (T1, T2, T3a plus two corollaries, T3b, T4). Lean reports three axioms.

Machine-checked for the voter model extracted by Aeneas from rust/src/lib.rs (#![no_std], no unsafe, no allocation, no loop, no recursion), not a hand-written model. Correspondence to the Rust source rests on Charon and Aeneas at the pinned versions. Not the cose-parse-nopanic product tree — this crate follows its layout and pins as a template only.

Watch

Needs: a browser.

CI: run ci, 2026-09-24 , executed by GitHub Actions, not by me.

You should see: jobs rust and lean, both green. rust binds the committed LLBC and generated Lean to the Rust source via sha256sum -c reports/PROOF.sha256, then runs cargo test. lean checks out Aeneas at the pinned commit, builds its Lean library, runs lake build VoterStatements, which builds VoterProof and QuadVoterProof transitively, checks the axiom sets of T1, T2, T3a (and its corollaries T3a_correct_never_disabled, T3a_nonempty), T3b, and T4 against {propext, Classical.choice, Quot.sound}, then runs the secondary, textual sorry/admit/axiom gate (scripts/check-no-sorry.sh, self-tested against eleven fixture cases first). Neither job runs Charon; neither re-extracts LLBC or generated Lean.

Would falsify: a failed job, or any axiom outside {propext, Classical.choice, Quot.sound} showing up in the unexpected axioms check.

You should see: 'VoterStatements.T4' depends on axioms: [propext, Classical.choice, Quot.sound] then extra axioms outside propext / Classical.choice / Quot.sound: (none) then PASS.

Would falsify: a fourth axiom or sorry in any axiom line, or extra axioms reporting anything other than none.

Typed replay of the verbatim local transcript of 2026-09-24 at pin b2cdeeb: every command shown is the literal command run, every output line is the literal output, mechanically split from a single raw capture (scripts/check-no-sorry.sh’s self-test, lake build’s own warnings from Aeneas’s vendored Std files, included as-is). One thing is dropped, not rewritten: Aeneas’s own \r-animated progress-bar spinner and its two volatile temp-path Info lines during scripts/check-extraction.sh, replaced by a bracketed note at that exact spot. Output timing is not execution timing. The viewer did not reproduce it.

Run

Needs: Rust (CI uses the stable toolchain via dtolnay/rust-toolchain@stable), Charon 909ff09a, Aeneas c2015b86, Lean 4.31.0 — same pins and machine as cose-parse-nopanic, install notes in reports/TOOLCHAIN.md.


git clone https://github.com/dzatona/quad-voter-proof.git && cd quad-voter-proof && git checkout b2cdeeb
sha256sum -c reports/PROOF.sha256
cd rust && cargo test
cd .. && export PATH="$HOME/charon/bin:$PATH"
scripts/check-extraction.sh   # re-extracts and diffs against the committed llbc/Lean
scripts/check-no-sorry.sh     # self-tests, then greps every lean/*.lean file
cd lean && lake build
lake env lean --stdin <<'EOF'
import VoterStatements
open VoterStatements
#print axioms VoterStatements.T1
#print axioms VoterStatements.T2
#print axioms VoterStatements.T3a
#print axioms VoterStatements.T3b
#print axioms VoterStatements.T4
EOF

You should see: lake build exit 0 and every #print axioms line showing only propext, Classical.choice, Quot.sound.

Would falsify: a non-zero exit from lake build, a hash checked by PROOF.sha256 reported FAILED, scripts/check-extraction.sh reporting a diff, or a fourth axiom (or sorry) in any #print axioms line.

Read

Needs: nothing to install.

reports/PROOF.sha256 binds the Rust source, Cargo.toml, Cargo.lock, lakefile.lean, the committed LLBC, the generated Lean, the handwritten proof/statements files, and the four verification scripts themselves (scripts/check-extraction.sh, scripts/normalize-llbc-diff.py, scripts/check-no-sorry.py, scripts/check-no-sorry.sh) to recorded hashes — an unnoticed edit to one of those scripts (say, a check-no-sorry.py that always reports clean) would otherwise silently defeat its own gate. scripts/check-extraction.sh re-extracts LLBC via Charon and diffs it, normalized rather than byte-for-byte (reports/EXTRACT.md explains why), against the committed llbc/quad_voter_proof.llbc and lean/QuadVoterProof.lean (Aeneas’s unedited output). Pins: Charon 909ff09a, Aeneas c2015b86, Lean 4.31.0 — TOOLCHAIN.md .

Theorems, all proved in lean/VoterStatements.lean over the code Aeneas extracted (built on equational characterizations proved in lean/VoterProof.lean):

T1 (no-panic): for every active set and every four command words, step returns ok — never a panic. ok includes every StepResult variant, including Undetermined and OutsideHypothesis — this is “no panic”, not “no undetermined result”.
T2 (masking, one step, arbitrary active set A): with |A| ≥ 3 and at most one active channel disagreeing with a claimed value v, step outputs v and disables exactly that one disagreeing channel (or nothing, if all agree).
T3a (reachable traces, no order assumption) and its corollaries T3a_correct_never_disabled, T3a_nonempty: on any trace from four active channels, with |F| ≤ 2 faulty channels and — every step — the active channels not in F agreeing on a value, a channel not in F is never disabled. False for an arbitrary starting state (a counterexample found during review: one correct channel outvoted by two agreeing faulty ones); stated only for traces starting at four active channels. T3a proves a correct channel is never disabled; it does not prove a command is issued when two channels disagree simultaneously by value (a 2–2 split at four active channels gives OutsideHypothesis, no command) — “survives two failures” is only the T3b statement below, with T3b’s own assumption.
T3b (reachable traces, with “faults reveal one at a time”): additionally assuming at most one faulty active channel disagrees with the correct value per step, the command is always that correct value, and the OutsideHypothesis result never occurs.
T4 (pair): with exactly two channels active and disagreeing, the result is an explicit Undetermined — no command, active set unchanged.

Axioms of all seven theorem statements (T1, T2, T3a and its two corollaries, T3b, T4): propext, Classical.choice, Quot.sound only, checked by #print axioms in CI. No sorry, no axiom, in any of the project’s Lean files — checked by scripts/check-no-sorry.sh, comment-aware (a sorry -- TODO or a private axiom cannot hide from it), self-tested against eleven fixture cases before it checks the real files.

The model: source vs. ours

Two open sources describe “Biser-4”, and they say different things. buran.ru (su4bcvk.htm) says: four channels, synchronous, same programs, an output comparison scheme monitoring all four channels’ commands, blocking a failed channel’s output, 4 → 3 → 2, rated for two failures in any path. Parondzhanov’s testimony corroborates “synchronous, same programs” and that synchronization was hardware, not software. Vikhorev–Glazkov (NPCAP, 2007) — a separate, independent primary source — say only that Biser-4 used fourfold redundancy for the two-failure-in-any-path requirement; they do not describe synchronous operation, identical programs, the comparison scheme, or blocking. Neither source says how the comparison scheme picks the failed channel, what it does with a disagreeing pair, or how inputs are distributed to the channels. Rules beyond what these sources state are marked “ours” in the project’s README and in rust/src/lib.rs’s doc comments — including: a blocked channel never returning (Biser-4’s predecessor “Biser-2” restored a lane after a transient upset by RAM copy; this model represents permanent failures, not recoverable upsets); the u64 command-word type (source words are ~36 bits; no built-in Rust type is exactly 36 bits); whole-word rather than bitwise comparison; and the exact behavior on a disagreeing pair (Undetermined) or any pattern outside “one disagreeing channel among an agreeing majority” (OutsideHypothesis).

Does not establish

Specification errors
Input congruence / a Byzantine command source
Synchronization, timing, the clock generator
The comparison-scheme hardware, the compiler, or any certification credit — this proves properties of the Aeneas-translated code only, and establishes no DO-178C or DO-330 qualification
A common flight-software bug — all four channels agreeing on a wrong command; the proved voter outputs it, by T2/T3b’s own conclusion
Upsets with recovery — this model’s disabled channels never return, a deliberate divergence from the “Biser” family, where “Biser-2” restored a lane by RAM copy after a transient upset
Survival past the third failure
Behaviour outside the failure hypothesis — OutsideHypothesis is the proved result, not a proved command
What a real implementation should do about an undetermined pair
Correspondence with the actual “Buran” implementation — theirs was hardware plus assembly, this is a from-scratch Rust model of the open-source description
Trust in the Lean kernel, Charon, and Aeneas as tools (none is qualified under DO-330)

More on the voter and why four channels rated for two failures on the article.

If this does not survive your check, write me.