Every AI model runs on a foundation so complex, and so entangled with proprietary components, that it can’t be verified — yet that same AI is being handed autonomy and pushed into critical systems faster than anyone can keep up.
trust chain closed · v1.3 · source-available
A compiler that builds itself from 299 bytes of hand-typed hex.
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 real language models — a modern SmolLM2 chat model and GPT-2 — verified token-for-token.
Why Helix exists
The problem, and what we do about it.
AI is being pushed into critical systems faster than anyone can verify it. Helix is the foundation you can actually check — every byte, end to end.
Helix is a from-scratch stack you can verify — auditable from 299 bytes of hand-typed hex all the way up to the GPU kernel — so any model you run on it can be checked and reproduced, end to end.
Verifiable execution
Real neural networks. Proof, not promises.
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.
GPT-2 124M · token-for-token 25/25 GPT-2-XL 1.5B · 25/25 · logit diff ≤ 4.4e-05 SmolLM2-135M (Llama arch, 2024) · 25/25 · ≤ 4.9e-05 byte-identical across runs · sha 8a2595cd… live GPT-2-XL ≈ 10 s/token today — trust first; faster as it matures
Replay · committed run
Watch the real run
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 outputsSee the proof
The proof dashboard: from-raw anchors, parity gates, byte-identical reruns, and the signed attestation each demo run writes.
demo/dashboard.html → The full storyWhat “verified” means here
Independent 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.
The bootstrap chain
Nine rungs. 299 bytes you have to trust.
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.
Three commitments
A foundation, not another framework.
Helix exists to remove uncertainty wherever software honestly can — every byte inspectable, every step reproducible, every limit stated plainly.
01
Source-available & fully auditable.
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 commercial revenue and industry partnerships.
Helix NC License v1.0source-available
02
Bootstrapped from raw binary.
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.
299 B → kovcK2 == K3 == K4
03
ML-first language design.
Forward- and reverse-mode autodiff are language features, not libraries. @pure is enforced at autodiff checkpoint boundaries, reflection is lowered at compile time, and the same compiler emits both x86-64 ELF and PTX for real GPUs.
grad / grad_rev_all@kernel → PTX
autodiff.hx · grad
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 }
kovc loss.hx -O2 → 7.0_f64
Autodiff, in the language
Gradients are a keyword, not a library.
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.@pureEnforced at autodiff checkpoint boundaries: a checkpointed function reaching effectful code is rejected.quote / modify_fVerifier-gated reflection: your verifier runs before any mutation commits.
In Helix, this compiles
A real systems language. With math notation.
Pattern matching, generics, traits, closures, tiles, reflection — every kovc build is gated by a 109-program feature corpus. Three samples:
fib.hx
fn fib(n: i32) -> i32 { if n < 2 { n } else { fib(n - 1) + fib(n - 2) } } fn main() -> i32 { fib(10) }
recursion→ 55
gpu_scale_rt.hx
@kernel fn gpu_scale_rt(a: f32, s: f32, n: i32) { let i = block_idx() * block_dim() + thread_idx(); a[i] = s[0] * a[i] }
@kernel → PTX, sm_86→ runs on the GPU
reflect.hx
fn always_true(_: i32) -> i32 { 1 } fn main() -> i32 { let h = Quote(0); modify(h, 42, always_true(0)); Splice(h) }
reflection · verifier-gated→ 42
By the numbers
Hard numbers, every one of them grounded.
Every figure here resolves to a committed file, gate output, or trust record — pull the repo and verify any of them.
299bytes
hex0 — the hand-authored trust root
9rungs
raw binary → kovc, each built only by the prior rung
1.py
exactly one committed Python file — a fenced oracle, never in the toolchain
109programs
feature corpus gating every kovc build
8kernels
kovc-emitted PTX set that runs GPT-2 124M → XL
25/25tokens
greedy continuation matches the independent oracle — GPT-2 & SmolLM2
4.9e-5max abs
SmolLM2-135M logit difference vs the oracle, across 49,152 logits
1.5Bparams
GPT-2-XL at fp32 on one 8 GB sm_86 GPU
Carbon meets silicon
Compile something honest today.
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.