Under the hood: how kola works

You don't need this page to write kola. It answers the questions people ask once they start using it: is there an interpreter, what backends and targets exist, which one ships, and can kola call C.

The pipeline

Source first goes through a lexer, which splits the text into tokens (names, numbers, punctuation), and a parser, which builds a syntax tree from them. Both are written by hand; the parser is recursive descent, one function per grammar rule. There are no parser generators, because the product of the front end is the diagnostic: every error cites a section of the card and proposes a repair, and that needs a parser written for the purpose. A resolver then links modules, the standard library and package dependencies into one program.

The checker comes next. It checks types and nominal regions, effect rows (inferring them for private functions), flow-sensitive linearity of resources and owning values, the mutability discipline and the view rule, exhaustive match, the purity of assert, region escape on returns and stores, the constant-time rules inside a ct fn, and the rule that no contract depends on an untrusted parameter. kola check runs all of it and stops there.

What comes out of the checker is lowered into KIR, a typed intermediate representation in which names are resolved, every node carries its type, and every safety obligation has already been decided. That decision is made by a small difference-bound prover built into the compiler. Four classes of obligation go through it: index and slice bounds, req preconditions, arithmetic overflow and ens postconditions. Each site is either proven, and its check disappears, or left as a run-time check that traps. Nothing is dropped silently. kola ir prints the IR with each decision and its reason, and kola report checks prints the same decisions as a per-function list. IR-0: the one place a check may be dropped covers this in detail.

Every compiled path takes its decisions about checks from KIR: the C backend, the own backend and the JIT. The interpreter walks the checked syntax tree directly, keeps every check, and serves as the reference the others are compared against. A function the IR does not lower yet still compiles and runs, with all of its checks kept at run time, and kola check prints a note saying how many items that applies to. kola check --require-analyzed turns the note into an error.

The compiler is written in Rust with no dependencies, apart from Cranelift, which is confined to its own crate. The standard library is embedded in the binary: a kola copied into an empty directory compiles and runs kola programs with nothing else installed, and the library cannot drift from the compiler that ships it. --std <dir> (or KOLA_STD) compiles against a different tree, which is how you work on the standard library itself. Editing std/ on disk without that flag changes nothing.

Two executors of one program

The interpreter is what kola run and kola test use. It is the reference implementation: it defines how the language behaves, and every backend is compared against it. It also re-checks at run time some things the checker already proved, such as resource linearity.

The interpreter runs with a JIT (just-in-time compiler): while the program runs, it compiles some functions to machine code and calls those instead of interpreting them. Functions whose effect row is empty (!{}) are compiled through Cranelift and called from the interpreter's own call path; everything else stays interpreted. The empty row is what makes this sound. A pure function is "arguments in, value out", so when compiled code would trap, it does not trap: it sets a flag and returns a placeholder value, and the interpreter discards the result and runs the call again interpreted. The trap the program sees is always the interpreter's own, with the same message, kind, site and domain recovery. A function that loops is compiled on its first call; one that does not waits until it has been called several times. --jit-report prints which functions were compiled and why others were refused, --no-jit gives the pure tree-walker, and kola test --oracle runs the tree-walker as a third leg and compares both other legs against it. The JIT pays off on long, arithmetic-heavy functions such as cryptography; on a suite of small helpers its compile cost may never be repaid.

The C backend generates C and a runtime header, kola.h, and hands them to a C compiler. kola run --native and kola test --native run a program this way, and kola build produces artifacts with it.

kola test runs every test on both and compares the results file by file. A disagreement exits with code 3, not as a note under a green line. --interp runs the interpreter alone (no C compiler needed, the fast loop while you work) and --native the C backend alone. A file that the native side declines to build because of a card rule (for example, an MMIO window under a hosted run) is reported as not comparable: the interpreted verdict stands and the summary says no comparison was made. A failure of the C compiler is always an error.

This differential is the main way compiler bugs are caught. It has one blind spot: it cannot see a defect present on both sides. A trap on one side and corrupted memory on the other is the case KIR was built to rule out by construction rather than by testing.

The C backend

The C backend covers almost the whole language and is the production build path. It reaches any target a C compiler or cross-compiler supports.

• kola build file.kl writes build/<name>.c, a header build/<name>.kh with the module's public functions, constants and types, the runtime header and an object file (machine code that still has to be linked into a program). --link <path> links an executable, with all of kola's own compiler flags supplied, so there is no cc line to copy into a build script.

• The C compiler is --cc=<path>, else $KOLA_CC, else cc. gcc and clang both work; flags that only one accepts are probed against the actual compiler. The optimization level defaults to -O3 and is selected with --opt; --cpu x86-64-v3 or --cpu native raises the instruction-set baseline.

• On a Linux host with clang, an executable links kola's own runtime in place of libc, the C standard library most programs depend on, producing a static binary: one file that needs no shared libraries installed on the target machine. --libc system uses the system C library instead. kola cc --target linux-x64|linux-arm64 is a C compiler driver for those libc-free targets from any host.

• --freestanding builds for bare metal, meaning code that runs with no operating system underneath, such as a kernel or firmware: no libc, a static bump allocator, and at most four external symbols (the panic handler k_panic, two clock hooks and an output hook), each needed only if the program uses it. A fully proven pure module needs none.

• Every emitted .c file begins with a provenance comment: the compiler version, the card version, a hash of the embedded standard library and a hash of every source module. The same inputs produce byte-identical output wherever the build runs.

• The C compiler step is cached in ~/.kola/cc-cache, keyed on the compiler, its arguments and every input byte. Set KOLA_CC_CACHE=off before timing the compiler.

Some standard-library functions have hardware legs: AES-NI and PCLMULQDQ, SHA-NI, CRC-32C and their AArch64 counterparts. A leg is a C or assembly symbol named in the function's signature with an hw clause. The kola body stays the definition: it is what the interpreter runs, what the checker proved, and what kola test --native checks the leg against. The leg is taken only on a CPU that has the listed features, after the function's req has been checked. --no-hw builds with the kola bodies only. Packages can declare legs of their own the same way.

The own backend

The own backend builds programs with no C compiler, assembler or linker. It is where kola is going: a standalone toolchain for x86-64 and AArch64 on Linux, macOS and Windows.

Its pipeline continues from KIR. KIR is lowered once into LIR, a lower-level form closer to machine code. LIR is in SSA form (static single assignment: every value is assigned exactly once, which makes optimizations simpler) over scalar virtual registers (an unlimited supply of named values that are later mapped onto the CPU's real registers). In LIR aggregates live in explicit stack slots, checks are explicit branches to a trap, and the target's calling convention (the platform's rules for which registers and stack slots carry arguments and results) is applied at every call. An optimizer runs over LIR (constant and branch folding, inlining, simplification, if-conversion, hoisting). Instruction selection (choosing machine instructions for each operation) and register allocation (assigning values to the CPU's registers) then target x86-64 or AArch64, and kola's own writers and linkers produce the executable file formats of Linux (ELF), macOS (Mach-O) or Windows (PE). A linker is the tool that combines compiled pieces into one runnable file; kola has its own, so no system ld is needed. Checks the prover discharged are never emitted, so the prover's work pays off directly in machine code.

How to use it:

• kola build --link <path> file.kl, with no C-specific flags, tries the own backend first for the host or --target. If the own backend refuses the program, the build goes through the C compiler instead and prints a note naming the refusal. Without a C compiler, the refusal is the answer.

• kola build --cross --target <triple> --link <path> uses the own backend only.

• kola test --own runs tests through the own backend with no C fallback, one test image at a time, on an x86-64 or AArch64 host.

The own backend does not cover the whole language yet. What it admits grows release by release, and anything it does not admit is refused before an artifact is written, with the reason. The C backend stays the reference for what a shipped program does.

Constant-time code is the reason the own backend existed before it was a toolchain. An optimizing C compiler is entitled to turn branch-free code into code that branches on a secret, and there is no flag that forbids it. The own backend controls every pass that touches a ct fn: on each compile it computes which parameter values and memory contents reach a branch, an address or a hardware divide, before and after optimization, and a ct fn whose set grew is emitted unoptimized instead. A separate build tool, heterobuild, compiles a file's ct functions with the own backend and everything else with the C backend and links them into one binary.

Other architectures. --cross --target also writes objects for riscv64, riscv32, mips64el, mips32el, armv7m (Thumb-2), loongarch64 and wasm32, in ELF, Mach-O, PE-COFF or wasm format (--format). These go through older per-architecture code generators that walk KIR directly and do not optimize; they serve targets with no C compiler available and act as further independent executors to test against. On the 32-bit targets usize is 32 bits and a u64 travels as a register pair. Traps in objects from every backend call the same k_panic symbol, so objects from different backends link together.

Cranelift and the browser

Cranelift (crates/kola-clif) is the engine behind the JIT. It can also emit deterministic x86-64 and AArch64 objects with no C compiler, which makes it one more executor to compare against. It is not a production build path.

The playground is the interpreter compiled to WebAssembly (crates/kola-wasm). The repository's web/playground page has an editor, the hands-on examples and buttons to check, run and test. Everything runs in your browser with the standard library embedded; there is no server.

Targets

What safety costs at run time

Overflow and bounds checks stay in native code unless the prover removed them, and a failed one is a trap, never undefined behaviour. In practice a check that never fires costs little. It is a well-predicted branch, and on the C path the C compiler often proves the same range again and folds the check away on its own. The value of a discharged check is mostly that it was proven at compile time rather than that the program runs faster. It pays in speed where a check would block vectorization or where the C compiler cannot see the bound, and it pays in review everywhere: kola report checks reaching "0 runtime" is a statement about the code.

Allocation shape matters more. A region is a bump arena: allocating is a pointer increment and freeing is dropping the arena at the brace, with no per-object bookkeeping. The failure mode is a region that outlives the work it serves. A server that allocates per request into a connection-lifetime region keeps every request's memory, and gets slower as well as larger, because the arena grows with every byte served. Open a region per request, or per loop iteration; its memory is returned at the brace. kola report leaks looks for allocations inside loops whose region outlives the loop; see Region leaks.

The repository keeps its measurements in docs/perf-notes.md, each with the machine, the compiler and the conditions. If you measure kola yourself, a few rules save time:

• Name the C compiler in every number. gcc and clang produce noticeably different code for the same emitted C, in both directions depending on the workload.

• Give a microbenchmark a live data dependency on every result, or the C compiler deletes the work you meant to time.

• Measure on an idle machine. A number taken next to a compile is noise.

• Measure the shape you ship. A one-line benchmark can be optimized in ways the full program is not.

• Turn the cc cache off (KOLA_CC_CACHE=off) when you time the compiler, and keep the default --opt level for any number you publish; a non-default level prints a note for this reason.

C and libc: no FFI

kola cannot call C functions. There is no extern "C", no FFI, no raw pointer type, no inline assembly and no unsafe block. The reason is that every guarantee kola makes ends at such an edge. The compiler can check effects, contracts and linearity in kola code, but not inside someone else's shared library, and an assembly body can corrupt memory where no oracle would notice. Keeping that edge closed is what lets Security describe a finite attack surface without exceptions.

What kola offers instead:

• Hardware legs for the cases where one instruction beats any amount of ordinary code, with the kola body kept as the definition and tested against the leg.

• Processes: to reuse an existing C program, run it with sys.proc.spawn under a grant.

• The other direction: C can call kola. kola build emits a header for a module's public functions, so a kola library can live inside a C program. See Embedding kola in a C program.

kola's own runtime needs no libc either; see the libc-free and freestanding targets above.

Development modes

Two kola run modes help while developing a service. kola run --reload <handler> applies checked edits at the next call of a named handler without restarting the process; state and capabilities survive, and an edit that fails to check leaves the previous code running. kola run --restart rechecks the whole program and starts a fresh process on Unix hosts, resetting local state. kola help reload has the details and the limits. For state that must survive a code change, LiveState[S] is a linear owner that migrates fixed-size data through explicit, pure conversion functions (STD-CARD, LiveState).

Editors and tooling

kola lsp is the language server, started by an editor rather than by hand. It serves diagnostics, document symbols and hover: a function's signature with its effect row and contracts, the type the checker inferred under the cursor, and a hint where checks stay at run time. It is part of the compiler, so the hover is the checker's own answer. Go-to-definition, references and rename are not supported yet. Editor clients for VS Code, Neovim and JetBrains (via LSP4IJ) are in the repository's editors/ directory and are installed from the checkout.

For tools and agents, kola query emits JSON maps built from the compiler's own facts: outline, symbol, callers, callees, effects, refs and attack-surface. kola mcp is an MCP server over the same facts, with a project index that can answer which code and which tests a change affects. The compiler also serves its own documentation: kola help spec-card, kola help std-card, kola help std-index and kola help ai, so a fresh machine needs nothing but the binary.