Salt

A systems language with Z3-powered compile-time verification. Write requires/ensures contracts — the compiler proves them with Z3. Provable checks have zero runtime cost; the rest become runtime assertions as a safe fallback. Arena memory, MLIR codegen. No GC, no borrow checker, no lifetime annotations.

package main

use std.core.result.Result

fn binary_search(arr: &[i64; 5], target: i64) -> Result<i64>
{
    let mut lo: i64 = 0;
    let mut hi: i64 = 4;
    while lo <= hi {
        let mid = (lo + hi) / 2;
        if arr[mid] == target { return Result::Ok(mid); }
        if arr[mid] < target { lo = mid + 1; }
        else { hi = mid - 1; }
    }
    return Result::Err(Status::from_code(5)); // NOT_FOUND
}

pub fn main() -> i32 {
    let data: [i64; 5] = [1, 3, 5, 7, 9];
    match binary_search(&data, 5) {
        Result::Ok(idx) => { return idx as i32; }
        Result::Err(_) => { return -1; }
    }
}

Z3 proves array bounds at compile time and elides the check. With loop induction variables, Z3 elides bounds checks for the entire loop body. The Result::Err path returns NOT_FOUND instead of a sentinel value.

Getting started

git clone https://github.com/bneb/lattice.git
cd lattice
make setup              # Install dependencies (once)
make build              # Build the compiler (~2 min)
make test               # All compiler unit tests pass (1323+)
make lettuce-verify     # Z3 contract verification tests pass
make bench              # LETTUCE vs Redis comparison

Prerequisites: Rust 1.75+, Z3 4.12+ (brew install z3), LLVM 21+ (brew install llvm@21), QEMU (brew install qemu).

Your first Salt program:

// hello.salt
package main

fn main() -> i32 {
    println("Hello, Salt!");
    return 0;
}

salt-front hello.salt --lib --disable-alias-scopes -o /tmp/hello && /tmp/hello

Full tutorial → — build a verified key-value store in 15 minutes.

Architecture

Salt Source (.salt)
    │
    ▼
Parser → Type Checker → Z3 Verifier → MLIR Emitter    [salt-front/]
    │
    ▼
mlir-opt → mlir-translate → LLVM IR → clang -O3       [LLVM backend]
    │
    ▼
KeuOS Kernel: boot.S → kmain → Drivers → Ring 3        [kernel/]
    │
    ▼
User Programs: LETTUCE, Basalt, FACET, NetD            [user/]

Full architecture reference →

What's here

Built with Salt

Verification

Salt embeds Z3 as a compiler pass. Functions carry requires and ensures clauses. The compiler translates them to Z3 formulas and checks them during normal compilation.

UNSAT — the condition always holds. The check is elided. Zero instructions.

SAT — Z3 found a counterexample. You get the specific values before your program runs.

TIMEOUT — Z3 cannot decide within 100ms. A runtime assertion is emitted. Your program still compiles and runs.

Verification is progressive: add the contracts you can prove today. The rest become runtime checks you can address later.

After compilation, Salt reports proof coverage:

Z3: 10/24 checks proven (41%), 14 deferred to runtime

Salt also provides automatic optimizations: the @ operator on Tensor types emits cache-tiled matrix multiplication with L1-sized blocks. On M4 Pro at 2048×2048 f64, Salt's tiled matmul runs in 1.06s vs. hand-tuned C at 1.12s (5.6% faster). Benchmarks →

Performance

LETTUCE, a 314-line Salt server implementing 9 Redis commands, was benchmarked against Redis 7 on the same machine using redis-benchmark. 13-point concurrency sweep, 50,000 requests per test.

LETTUCE leads at every concurrency level. The structural advantage is the arena allocator — zero malloc per request vs. Redis's zmalloc/zfree contention under load. Full benchmark data →

Further reading

• Tutorial: Your First Verified Program — 15-minute walkthrough
• Blog: Zero-Cost Safety — Z3 contracts at compile time
• Blog: Microkernel IPC — SPSC rings, zero-copy, proof-carrying IPC
• Blog: Arenas Over Borrow Checking — Scope Ladder escape analysis
• LETTUCE vs Redis — benchmark data and analysis
• Architecture Reference — compiler pipeline, kernel design, memory model
• Language Specification — formal language definition
• Contributor Guide

License

MIT