Keel

A systems language built for agents first. If a program compiles, it has been proven free of integer overflow, out-of-bounds access, division by zero, contract violations, data races and non-termination. Because every safety property is proven up front, the generated code has no runtime checks at all.

Results so far

• As fast as Rust, with proofs. Counting primes below 20M with par: 0.23 s against 0.20 s for Rust scoped threads. Mergesort of 10M integers: 0.12 s, the same as rayon::join, with the output proven sorted and a permutation of its input.
• Learnable by agents from one page. Haiku, Sonnet and Opus each wrote verifying Keel from a one-page primer. Given the contract, all three proved all six exact specifications in round 2 (18 of 18). Their Rust solutions passed the same hidden tests while carrying no machine-checked facts (evals).
• Deterministic. Every check gets a fixed budget of solver work, so with the same Z3 version the same file gets the same verdict on every run and machine.

Can you break it? If you get a program past keel check that overflows, indexes out of bounds, races or loops forever, that is the most valuable bug report there is. See BREAK_IT.md for what counts and where we think the weak spots are.

Install

Prebuilt binaries for macOS (Apple Silicon, Intel) and Linux (x86_64, arm64) are on the releases page. For example, on an Apple Silicon Mac:

curl -sSL https://github.com/swperb/keel/releases/download/v0.1.0/keel-v0.1.0-aarch64-apple-darwin.tar.gz | tar xz
sudo mv keel-v0.1.0-aarch64-apple-darwin/keel /usr/local/bin/

Or build from source with Cargo:

cargo install --git https://github.com/swperb/keel

Keel needs Z3 on PATH and a C compiler (cc, or set CC). Keel is tested with Z3 5.3.2: brew install z3, or a binary from Z3's releases. Older distribution packages (Ubuntu 24.04 ships 4.8.12) are too slow for some proofs. Then:

keel check file.kl    # prove
keel run file.kl      # prove, compile, run

A taste (examples/search.kl):

fn search(xs: &[i64], key: i64) -> i64
  requires forall i in 0..len(xs) { forall j in i..len(xs) { xs[i] <= xs[j] } }
  ensures result == -1 || (0 <= result && result < len(xs) && xs[result] == key)
  ensures result == -1 ==> forall k in 0..len(xs) { xs[k] != key }
{
  var lo: i64 = 0;
  var hi: i64 = len(xs);
  while lo < hi
    invariant 0 <= lo && lo <= hi && hi <= len(xs)
    invariant forall k in 0..lo { xs[k] < key }
    invariant forall k in hi..len(xs) { xs[k] > key }
    decreases hi - lo
  {
    let mid: i64 = lo + ((hi - lo) / 2);
    ...

Why agents

Humans want terse syntax and flexibility. Agents want the opposite: one obvious way to write each thing, local reasoning, and a compiler that says exactly what is wrong. Keel is designed around that.

Goal	How Keel gets there
Strictest verification	Every function is symbolically executed and each risky operation becomes an SMT proof obligation (Z3). Unproven means rejected. There is no assume, no unsafe, no escape hatch.
Rust speed	Compiles to C11 at -O3. No GC, no runtime checks, &mut borrows lower to restrict pointers. Benchmarks match hand-written Rust.
Go-sized design space	One loop (while, which must state a decreases measure), one conditional, no ternary, no shadowing, no operator precedence, no overloading, no implicit conversions, no macros, no exceptions, no null, no globals.
Economical	Zero-dependency compiler. Tiny runtime (alloc + a core-bounded spawner). Memory freed deterministically at scope exit. No warmup, no heap tuning: the program is as fast on a small box as it will ever be per core.
Agent feedback	Stable error codes, --json output, and concrete counterexamples from the solver (a = -1, b = -9223372036854775808). keel explain CODE gives the long form.

No precedence, on purpose

a + b * c is a compile error (E-PAREN). So is a && b || c. You write a + (b * c). Chains of one associative operator are fine. Bitwise operators follow the same rule: a & b | c and a + b << 2 are errors. This removes an entire class of misreadings, for models and people alike.

Compared to Bend

Bend (bend-lang.com, v2.0.39 at the time of writing) describes itself as having a proof-checking type checker in the style of Lean and Rocq, built on an affine dependent type theory, near-C speed on one core, and automatic parallelism across CPU cores and GPUs. We have not benchmarked Bend ourselves, so this section only makes claims about Keel that we measured or that the compiler enforces:

This is the beginning of the README. Read the rest at the original. Read the full README ↗