Helix is a from-scratch, ML-native systems language — autodiff, tile types and GPU codegen built into the language, bootstrapped from raw binary with no trusted pre-built compiler. And it runs the real GPT-2, verified token-for-token.
GPT-2 — the real, unchanged public model — runs on this stack token-for-token-identical to an independent reference. So does a 2024 Llama-architecture model. Bring your weights; audit instead of trust.
A replay of a real, captured GPT-2-on-Helix session — clearly labeled, never simulated. The models are 2019/2024 base completion models, not assistants.
demo/ → Proof · gate outputsThe proof dashboard: from-raw anchors, parity gates, byte-identical reruns, and the signed attestation each demo run writes.
demo/dashboard.html → The full storyIndependent numpy oracle, fail-closed gates, honest residuals — the precise claim, stated edge-first, and how a third party reproduces it.
Verifiable execution →The models were verified by fail-closed gates on real hardware; this website runs nothing live — it links to committed replays and gate records.
Each rung is built only by the rung before it — no pre-built compiler is ever trusted. Select any node to inspect it; one committed command reproduces the whole ladder.
Helix exists to remove uncertainty wherever software honestly can — every byte inspectable, every step reproducible, every limit stated plainly.
The entire toolchain is inspectable, from the 299-byte hand-typed root to the PTX it emits. Free for non-commercial use — individuals, students, researchers, non-profits — under the Helix Non-Commercial License; commercial use requires the author's consent. Not open source yet: a restriction intended to be temporary while the project secures investors, revenue, and industry partners.
No trusted pre-built compiler, anywhere. The hex0 root is 299 hand-authored bytes of x86-64; nine rungs compile each other up to kovc, the Helix compiler written in Helix — with a byte-identical self-host fixpoint and no Python in the toolchain.
Forward- and reverse-mode autodiff are language features, not libraries. Tiles and tensors are types. Effects are verified at the IR level, reflection is verifier-gated, and the same compiler emits x86-64 ELF and PTX for real GPUs.
fn loss(x: f64, y: f64) -> f64 { x * y + x * x } struct Grad { dx: f64, dy: f64 } fn main() -> f64 { // reverse-mode AD, all gradients in one sweep let g = grad_rev_all(loss)(2.0_f64, 3.0_f64); g.dx }
Forward- and reverse-mode autodiff lower into the program at compile time — no runtime tape, no tracing, no Python overhead. Stdlib transcendentals carry analytic chain rules.
grad(f)(x)Forward-mode derivative. Symbolic, fully inlined.grad_rev_all(f)(...)Reverse-mode adjoints; returns a struct of all partials.@pureIR-level effect verification — pure functions are transitively barred from effectful code.quote / modify_fVerifier-gated reflection: your verifier runs before any mutation commits.Pattern matching, generics, traits, closures, tiles, reflection — every kovc build is gated by a 109-program feature corpus. Three samples:
fn fib(n: i32) -> i32 { if n < 2 { n } else { fib(n - 1) + fib(n - 2) } } fn main() -> i32 { fib(10) }
fn main() -> f32 { let a = tile<f32, [4, 4], REG>::ones(); let b = tile<f32, [4, 4], REG>::ones(); let c = tile_matmul(a, b); c.get(2, 3) }
fn always_true(_: i32) -> i32 { 1 } fn main() -> i32 { let h = Quote(0); modify(h, 42, always_true(0)); Splice(h) }
Every figure here resolves to a committed file, gate output, or trust record — pull the repo and verify any of them.
Rebuild the entire compiler from 299 hand-typed bytes with one committed command — then watch the real GPT-2 run on it, verified token-for-token against an independent reference.