Salt language uses Z3 theorem prover to verify systems code at compile time

Salt is a new programming language for high-performance computing

A new programming language called Salt has launched, promising mathematically proven safety for systems programming without runtime overhead. It aims to replace languages like C and Rust in performance-critical domains such as AI inference, operating systems, and databases.

The language uses the Z3 theorem prover to verify function contracts at compile time. Developers write `requires()` and `ensures()` conditions, and the compiler either confirms they hold for all inputs or fails the build.

It was built for and tested on demanding real projects

Salt was developed by solving concrete, high-performance computing challenges. Its creators have used it to build several demanding systems as proof of concept.

• Llama 2 Inference Engine: A complete 600-line engine that memory-maps weights and uses Z3 to prove kernel array accesses are in bounds.
• Lattice Unikernel: A from-scratch operating system kernel that boots on real x86 hardware with its own scheduler and drivers, with no C runtime or libc.
• Lettuce: A Redis-compatible datastore written in 567 lines of Salt that handles 234,000 ops/sec, roughly double the throughput of Redis itself in their tests.
• FACET: A full-stack 2D rendering engine where every pixel write carries a Z3 proof it's within the framebuffer.

The language combines formal verification with arena allocation

Salt's design rests on three core ideas: formal verification, region-based memory management, and leveraging the MLIR compiler framework.

Instead of a garbage collector or a borrow checker, Salt uses arenas. All allocations happen within a region, and the entire region is freed at once. The compiler verifies that no reference outlives its arena.

For performance, Salt emits code through MLIR, the same infrastructure behind TensorFlow. This allows for automatic, hardware-optimized instruction selection. The creators claim their Z3-verified matrix multiplication runs 6.8x faster than code compiled with `clang -O3`.

It offers ergonomics inspired by modern languages

The syntax includes pipelines with a `|>` operator for chaining and `|?>` for error propagation. It uses f-strings for formatting, which are type-checked at compile time and don't allocate.

Unverified code is explicitly marked. Raw pointer arithmetic is inside `unsafe` blocks, and foreign function calls use an `@trusted` attribute.

The language ships with a package manager called `sp` and over 70 modules with zero external dependencies. When a library declares a `requires()` contract, the compiler verifies it at every downstream call site.

Benchmarks show it matches or beats C and Rust

The team publishes benchmarks comparing Salt to C (`clang -O3`) and Rust (`--release`) on 22 tasks. They claim Salt matches or outperforms both on all benchmarks when run on identical hardware.

Their methodology uses dynamic inputs and prints results to prevent dead-code elimination. One benchmark, run on an Apple M4, shows Salt's performance is algorithm-identical to a C reference, matching `clang -O3` at 457 fps for a graphics task.