A machine-facing portable assembly.
Faster than C.
Krell is a program representation that sits between assembly and C: the raw power and speed of assembly, with the portability of C — designed from the start for machines, not humans, to produce and consume. Producers are compilers, superoptimizers, and automated agents.
Apache-2.0 · Toolchain output carries no license obligations · C11, no dependencies beyond libc / libm
x86_64 native, geometric mean
1.81× native · 1.59× LLVM (59%)
x86_64 and LLVM lanes
x86_64 · AArch64 · RISC-V 64 · LLVM
one program, written once ──► Krell-IR (binary, hashed, verified)
├── x86_64 native backend
├── AArch64 native backend
├── RISC-V native backend (RV64)
└── LLVM IR lowering lane (release)
Designed for machines
Every choice in Krell serves a machine producer and a machine consumer: a format that is cheap to emit, cheap to verify, and impossible to misread.
Typed SSA with block arguments
Infinite virtual registers, explicit blocks, no phi nodes — the form four independent IR designs converged on, because it is the one that works.
Total semantics — no undefined behavior
Every operation is defined for every input. Division by zero is 0, shifts mask their amount, float→int saturates and maps NaN to 0. No poison, so translation validation stays decidable.
Backend-owned ABI
Backends own register allocation, instruction selection, and the C calling convention for their target. Producers never reimplement an ABI.
Curated op set, no cliffs
The instruction set is the intersection of operations efficient on every target, plus predicated escape hatches where that intersection is empty.
A shipped cost oracle
Every target carries a machine-readable cost table: latency, throughput, and cliff flags. The verifier rejects cliff operations for a target; the optimizer prices rewrites from the same tables.
Machine-first binary encoding
Canonical, hash-consed, and content-addressed: a module's SHA-256 over its canonical encoding is its identity. Round-trips are byte-identical by construction.
A reference interpreter
The semantics document made executable. Every backend is differentially tested against it.
Optimizer + superoptimizer
A rewriting optimizer with magic-number division and dead-code elimination, plus a bounded fragment superoptimizer in tools/.
Performance
Measured against C (gcc, -O2) on the twelve KRELLPROOF kernels — the same workloads written once in Krell and once in C, timings recorded only where the implementations' checksums agree. S is the per-kernel speedup TC / TKrell; figures are geometric means from the WP18 record, 2026-11-04.
| Lane | S, all twelve kernels | S, excluding fib |
|---|---|---|
| x86_64 native | 4.91× — 391% faster than C | 1.81× — 81% faster than C |
| LLVM | 4.67× — 367% faster than C | 1.59× — 59% faster than C |
fib is quoted both ways because it dominates any mean it joins: the optimizer lowers its two-term recurrence to an O(n) loop. The full record — kernels, C references, methodology, per-run results and charts — lives in the krellproof repository.
Get started
The toolchain is C11 with no dependencies beyond libc and libm. It builds clean under -Werror.
# Build git clone https://github.com/nightwarelabz/krell cd krell make # libkrell.a + krellc make tests # kernel suite + binary round-trip gate # Use krellc parse prog.txt -o prog.krel # surface syntax -> binary krellc verify prog.krel --target riscv64 # verify + target gate krellc run prog.krel sumsq 100 # interpret: 338350 krellc build prog.krel --target x86_64 -o prog.s krellc build prog.krel --target llvm -O -o prog.ll krellc opt prog.krel -o prog.opt.krel # optimize krellc hash prog.krel # canonical module identity
The Krell ecosystem
Krell is the foundation. These projects are built on it — a kernel, an operating system conversion, a compressor, and a music engine, all in pure Krell.
K0
A kernel written in pure Krell for x86_64 and AArch64 — console, allocator, scheduler, storage, networking, and native module execution.
github.com/nightwarelabz/k0 →Krellinux
The Linux kernel converted from C to Krell — the mainframe core, reinvented function by function with differential proof at every step.
github.com/nightwarelabz/krellinux →krellstd
zstd in Krell: the standard compression format, reimplemented on a representation built for exactly its copies, tables, and bitstreams.
github.com/nightwarelabz/krellstd →KRELLPROOF
The benchmark harness: C references, methodology, recorded results, and charts behind every performance number on this page.
github.com/nightwarelabz/krellproof →Krellophone
The pure-Krell music engine and its compositions — synthesis, scores, and films computed entirely by Krell programs.
github.com/nightwarelabz/krellophone →Specification
Language and binary-format specification, plus the normative semantics document — small enough to encode, total by design.
docs/SPEC.md →License
Apache-2.0, with the Krell Encoding Exception. Toolchain output carries no obligations: programs encoded in Krell form, and code produced by compiling them, are outputs of the toolchain. You may use, modify, and distribute Krell-encoded programs and their compiled forms under any terms you choose.