What question did this study set out to answer?

This research aims to present a comprehensive stack for ternary computing that is formally verified, ensuring reliability and correctness from machine code to kernel.

April 11, 2026Open Access

Σ₉ (9-Sigma) Formally Proven Ternary Language & Bare-Metal Stack Trithon: A Formally Verified Ternary Computing Stack from Lambda Calculus to Microkernel

Key Points

This research aims to present a comprehensive stack for ternary computing that is formally verified, ensuring reliability and correctness from machine code to kernel.
Developed a ternary machine code model with a 24-trit word architecture.
Created a strongly typed high-level language that supports ternary logic.
Established a verified six-pass compiler pipeline with semantic preservation.
Implemented a capability-based microkernel achieving Σ9 assurance.
Conducted formal proofs across various components to ensure system reliability.
Achieved Σ9 assurance with zero admitted errors, exceptions, and faults.
Encompassed 86 Lean 4 proof obligations across multiple aspects of the system.
Demonstrated effective end-to-end verification principles for ternary systems.
Outlined the proof effort relative to another verified kernel (seL4).

Abstract

Abstract. We present Trithon, the first formally verified computing stack built entirely on balancedternary arithmetic and three-valued logic. The system comprises five layers: (1) a ternary machine-codemodel with 24-trit word architecture and FPGA-validated ALU truth tables; (2) a macro assembler withmnemonic ISA and five reduction-rule instruction classes; (3) a strongly typed, purely functional high-level language extending Plotkin’s PCF with native ternary branching and a novel grade-polymorphictype system; (4) a six-pass verified compiler pipeline with semantic preservation proven at every passin the style of CompCert; and (5) seT9, a capability-based microkernel achieving Σ9 assurance—zero Admitted, zero sorry, zero exceptions—across both Rocq 9.1.1 and Lean 4 4.28.0 with Math-lib v4.28.0. The full formal stack encompasses 86 Lean 4 proof obligations spanning 19 algebraic, 9core-calculus, 9 type-system, 22 type-safety, 22 normalization, and 5 consistency lemmas plus 2 inte-gration theorems. We discuss the design principles that make end-to-end ternary verification tractable,compare the proof effort with that of seL4, and outline the path to deployment on emerging ternarysilicon from Samsung, Huawei, and others.

Read Full Paperexternally

Ask AI

Helpful

Bookmark

View Full Paper