El orbiter soviético Buran, lanzado en 1988, utilizó un sistema de computación redundante compuesto por cuatro unidades idénticas Biser-4, a diferencia de los esquemas de tres canales estándar. Esta configuración no se basaba en el teorema de los generales bizantinos (3f + 1), sino en un esquema de comparación de salidas que permitía detectar fallos y bloquear canales defectuosos. El diseño debía sobrevivir a cualquier combinación de dos fallos, una exigencia que la redundancia de cuatro canales cumplía de manera más robusta que la de tres en este contexto específico.
El artículo analiza las fuentes históricas y técnicas disponibles, destacando que la sincronización se realizaba mediante hardware para garantizar la fiabilidad, ya que la sincronización de software era considerada insuficiente. Se examina también la limitación inherente de copiar programas idénticos, citando fallos históricos como STS-1 o Ariane 501, y propone la disimilitad como solución industrial. Finalmente, el autor detalla su trabajo en Lean 4 para verificar teoremas sobre un votador en Rust, demostrando cómo las pruebas formales pueden validar componentes críticos, aunque señalando que estas herramientas no están certificadas bajo estándares de aviación como DO-330 o DO-178C.