Salt is a systems programming language that embeds the Z3 SMT solver in the compiler.
You add `requires` and `ensures` clauses to functions, and the compiler proves them at compile time. When Z3 succeeds, the check is elided (zero instructions emitted).
When it fails, you get a counterexample. When it times out (100ms limit per obligation), the check is skipped and counted.
It compiles through MLIR to LLVM and targets KeuOS, a microkernel with an ECS (Entity Component System) architecture. Both are MIT-licensed.
The key difference from Rust/Zig/C: the compiler calls Z3 during normal compilation. No separate verification tool, no annotation language, no proof assistant. The contract syntax is part of the language.
---
What's real
- Compiler: 1,752 unit tests passing, clippy clean. Compiles through MLIR to LLVM IR. x86-64 and ARM64 backends.
- Kernel: 14/14 QEMU e2e tests pass. TCP stack (connect/send/recv/close), ICMP, deterministic builds. NetD (network daemon) runs as a Ring 3 process on SPSC shared memory rings.
- ECS architecture: 13 entity syscalls (402-413). Entity lifecycle (spawn/exit/wait), memory regions as entities (map/brk/alloc), I/O routing via capabilities, socket entity tracking, performance counters, world persistence diagnostics.
- Shell: Inline `ecs`, `ps_ecs`, `free_ecs` commands query ECS World without spawning child processes.
- Benchmarks: Salt vs C (`clang -O3`) on 21 algorithm benchmarks. Salt at parity or faster on 19/21. Allocation-heavy workloads (hashmap, LRU, buffered writer) see 2-10x wins from arena allocation. Compute-bound (matmul, sieve, fib) at 0.9-1.0x of C.
- LSP: VS Code extension ships with semantic tokens, go-to-def, find-refs, Z3 hover.
---
What's not done (research-quality, not production)
- The standard library is incomplete. Many things you'd expect are missing.
- Z3 handles integer arithmetic, bit-vectors, and reals. String and quantifier support is partial. Contracts outside Z3's reach are compile-time checked where possible, silently skipped otherwise.
- Error messages from the Z3 pass can be opaque.
- The kernel targets QEMU (x86-64). Tested on AWS bare metal instances, not local 'bare metal' yet.
- One nights-and-weekends developer.
---
Why this exists
The goal was to find out whether formal verification could be a compiler feature rather than a separate toolchain. The benchmarks say the compiler is fast enough (Lettuce compiles in under a second with contracts enabled). The kernel contracts catch real bugs. But the language hasn't been used by anyone outside the project, and that's the test that matters.
You could nitpick the subsection title, and from that perspective "What's not done" is a bit of a catch-all for caveats.
With that said, I think it's pretty easy to infer the meaning there.
I'm not really sure how else to be more transparent about things, but I am using an AI-augmented engineering as the core workflow for the project, and that includes drafting docs and this post.
I read and edit the work. For a side-project with no current community support or users, I need to make a judicious decision when to spend time and effort. IMO it is reasonable _not_ to try to trick anyone into thinking that AI is not used. My proof reading and editing will miss things from time-to-time. I'm OK with it at the current scale of the project.
You add `requires` and `ensures` clauses to functions, and the compiler proves them at compile time. When Z3 succeeds, the check is elided (zero instructions emitted).
When it fails, you get a counterexample. When it times out (100ms limit per obligation), the check is skipped and counted.
It compiles through MLIR to LLVM and targets KeuOS, a microkernel with an ECS (Entity Component System) architecture. Both are MIT-licensed.
---
How it works
Call `safe_div(x, 7)` and Z3 proves `7 != 0`. Check elided.
Call `safe_div(x, 0)` and the compiler stops.
The key difference from Rust/Zig/C: the compiler calls Z3 during normal compilation. No separate verification tool, no annotation language, no proof assistant. The contract syntax is part of the language.
---
What's real
- Compiler: 1,752 unit tests passing, clippy clean. Compiles through MLIR to LLVM IR. x86-64 and ARM64 backends. - Kernel: 14/14 QEMU e2e tests pass. TCP stack (connect/send/recv/close), ICMP, deterministic builds. NetD (network daemon) runs as a Ring 3 process on SPSC shared memory rings.
- ECS architecture: 13 entity syscalls (402-413). Entity lifecycle (spawn/exit/wait), memory regions as entities (map/brk/alloc), I/O routing via capabilities, socket entity tracking, performance counters, world persistence diagnostics.
- Shell: Inline `ecs`, `ps_ecs`, `free_ecs` commands query ECS World without spawning child processes.
- Benchmarks: Salt vs C (`clang -O3`) on 21 algorithm benchmarks. Salt at parity or faster on 19/21. Allocation-heavy workloads (hashmap, LRU, buffered writer) see 2-10x wins from arena allocation. Compute-bound (matmul, sieve, fib) at 0.9-1.0x of C.
- LSP: VS Code extension ships with semantic tokens, go-to-def, find-refs, Z3 hover.
---
What's not done (research-quality, not production)
- The standard library is incomplete. Many things you'd expect are missing.
- Z3 handles integer arithmetic, bit-vectors, and reals. String and quantifier support is partial. Contracts outside Z3's reach are compile-time checked where possible, silently skipped otherwise.
- Error messages from the Z3 pass can be opaque.
- The kernel targets QEMU (x86-64). Tested on AWS bare metal instances, not local 'bare metal' yet.
- One nights-and-weekends developer.
---
Why this exists
The goal was to find out whether formal verification could be a compiler feature rather than a separate toolchain. The benchmarks say the compiler is fast enough (Lettuce compiles in under a second with contracts enabled). The kernel contracts catch real bugs. But the language hasn't been used by anyone outside the project, and that's the test that matters.
---
Links
- Source: https://github.com/bneb/lattice)
- Tutorial: https://github.com/bneb/lattice/blob/main/docs/tutorial/your...
- Architecture: https://github.com/bneb/lattice/blob/main/docs/ARCH.md
- Benchmarks: https://github.com/bneb/lattice/blob/main/benchmarks/BENCHMA...