Song

Song minimises the trusted computing base by building every layer from a small auditable seed and checking contracts at each layer.

The seed is songc0.s, 3,471 lines of pinned x86-64 assembly. Above it the compiler is written in Slang and compiles itself; the gen3 and gen4 binaries are byte-identical, a compiler fixpoint. That establishes reproducibility, not correctness, and the two are tracked separately.

§Components

• Slang. A small core grammar in which recursion is the loop. Bounded loop and while are surface syntax added in gen2.
• Native backend. Emits x86-64 machine code directly; no LLVM or GCC backend.
• Decider. A simplex-based linear integer arithmetic decider with replayable certificates. Functions carry law, spec and test blocks whose obligations it discharges.
• Kernel. Memory model, scheduling, trap handling, a content-addressed store.

§Relation to Apeiron

Song and Apeiron implement the same primitives independently, in Slang and in Rust, with no runtime linkage between them. The required result is a proof that both refine the same canonical Lean definitions. That correspondence is open.

Song currently runs as hosted Linux ELF binaries; bare-metal boot is a later milestone. CAVEATS.md in the repository lists what the verification does not cover.