Coherence Language
A language whose compiler proves its own output. Explicit effects, identity as a first-class type, one source across seven targets, and a certified path where the shipped artifact is proven to compute exactly what the source says.
All inputs
equivalence proved by solver across the whole input space, not sampled by tests
7
compile targets from one source: native, LLVM, VM, Python, WebAssembly, GPU, Luau
1,471
test files in the compiler and toolchain
29
cryptographic gates verified byte-exact against NIST and RFC test vectors
Availability. Coherence Language is the internal foundation the whole lab is built on, and is not yet publicly released: no public download or repository yet. You can watch it run live and reach into it in the browser demos (edit a .cl kernel, compile it to a GPU shader, and check that the results agree bit for bit), and request early access to the compiler and documentation. This page is the honest state of the language, not a marketing sheet.
The Core Guarantee
The compiler proves its own output
Every compiler you have ever used is trusted. You read the source, the tests pass, and you assume the binary does the same thing. Between those two lies an entire class of bug that testing cannot reach: the source is right, the tests are green, and the emitted code is subtly different.
Coherence closes that gap by proof. On the certified path, a solver is asked whether the optimized program and the original compute the same function for every possible input, not for a sample. When the proof does not go through, the build fails closed rather than shipping. The guarantee composes: superoptimization, compilation, and pipeline each carry it forward, so the artifact that ships is transitively bound to the source you read.
The same symbolic engine proves two versions of a function equivalent before an optimization is allowed to land, and synthesizes machine-checkable proofs from the result.
What the guarantee covers
Compiler Physics
Importance is computed, not profiled
Optimizing compilers normally need profiling runs to learn which code matters. Coherence solves a field instead. The same screened-Helmholtz equation the lab uses across the stack is solved over the program's own graph, and the resulting field drives instruction scheduling and register allocation.
Why it matters: the compiler reasons about structure directly, without needing a representative workload to profile first.
Included, Not Imported
A complete cryptographic suite, written in the language
Symmetric ciphers and authenticated encryption, key derivation, message authentication, hashing, elliptic-curve signatures and key exchange, and post-quantum signatures and key encapsulation: all implemented natively and verified byte-exact against NIST and RFC known-answer vectors, with identical results across four independent execution surfaces.
What It Is
Why we built a language at all
Coherence Language is the language stack behind the lab. We built it because ordinary languages treat effects, identity, governance, and runtime boundaries as conventions or libraries instead of part of the language itself.
We needed one language that could describe pure computation, governed runtimes, compilers, and site generation from the same surface, then compile that surface across browser, GPU, VM, native, and Python paths.
Coherence Language snapshot
// effects and identity are part of the language,
// not a convention bolted on later
fn transfer(from: Account, to: Account, amount: Money)
-> Receipt @ L2 effects [Ledger, Identity] {
require(from.balance >= amount);
let who = identity.current(); // who is acting is first-class
ledger.debit(from, amount);
ledger.credit(to, amount);
Receipt { by: who, moved: amount }
}Where It Fits Best
What Coherence Language is really good at
Next