For people looking for other languages with statically checked contracts, you might want to check out SPARK, which has been around in some form since the late 1980s. It is a subset of the Ada language and had been used for safety critical code in aerospace and defense projects, as well as for some Nvidia firmware.
It also uses Z3 to discharge proof obligations generated by the contract annotations, and it lets you use swap out different theorem provers as backends.
The GNAT Ada compiler (which is part of GCC) allows you to turn off the dynamic safety checks that are usually inserted into Ada programs at build time so you can optionally remove them if they are proven unnecessary.
Yes, it has generics. The syntax is Pascal-like, which some people used to C-family languages dislike but I personally find nice. Performance can definitely match performant C code. (intended use cases include real-time systems and embedded devices)
This looks pretty impressive but it’s all AI-generated (or written in a similar style) and therefore the documentation is lacking.
There is a language specification [1][2] but it lacks coherence.
I think the way to improve it would be to try to teach this language to people and get feedback from them. That is, it needs beta testers. It looks like there’s no community of users yet?
For complete transparency: AI augmented engineering is the core workflow for this project.
I have been pretty diligent about trying to de-slop the project after long RALPH loops and `/goal` prompts, and I review and edit documentation. Based on your feedback, I just made another pass.
Please feel free to let me know if there is anything specific lacking from the docs, and I will update them in the future.
If you compare say, the Go language specification for an assignment statement [1] to Salt's explanation of its let statement, there is a big difference. Salt's docs lean heavily on "it works like you would expect from other languages" so you have to reason by analogy. A specification shouldn't work that way; it should actually explain the rules for each language construct, without assuming knowledge of other languages.
> [int overflows, etc.] No runtime cost when Z3 can prove it. Otherwise, the compiler emits a safe runtime check as fallback.
Super interesting approach. I see this eventually be integrated into future mainstream languages, though that may take a while. I suspect that the game programming crowd will try to use it first, due to the possibility to prove certain edge cases at compile time and skip the runtime cost. But perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays. I may be too old for these predictions. Cool nonetheless.
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.
For people looking for other languages with statically checked contracts, you might want to check out SPARK, which has been around in some form since the late 1980s. It is a subset of the Ada language and had been used for safety critical code in aerospace and defense projects, as well as for some Nvidia firmware.
It also uses Z3 to discharge proof obligations generated by the contract annotations, and it lets you use swap out different theorem provers as backends.
The GNAT Ada compiler (which is part of GCC) allows you to turn off the dynamic safety checks that are usually inserted into Ada programs at build time so you can optionally remove them if they are proven unnecessary.
Here are some resources for comparison:
- https://www.adacore.com/languages/spark
- https://learn.adacore.com/courses/intro-to-spark/chapters/01...
SPARK seems interesting. Any ideas how it compares to Salt?
- C performance? - Generics? - Syntax ergonomics?
Thanks for sharing!
Yes, it has generics. The syntax is Pascal-like, which some people used to C-family languages dislike but I personally find nice. Performance can definitely match performant C code. (intended use cases include real-time systems and embedded devices)
The language overview can be found here: https://docs.adacore.com/spark2014-docs/html/ug/en/spark_201...
This looks pretty impressive but it’s all AI-generated (or written in a similar style) and therefore the documentation is lacking.
There is a language specification [1][2] but it lacks coherence.
I think the way to improve it would be to try to teach this language to people and get feedback from them. That is, it needs beta testers. It looks like there’s no community of users yet?
[1] https://github.com/bneb/lattice/blob/main/docs/SPEC.md
[2] https://github.com/bneb/lattice/blob/main/SYNTAX.md
For complete transparency: AI augmented engineering is the core workflow for this project.
I have been pretty diligent about trying to de-slop the project after long RALPH loops and `/goal` prompts, and I review and edit documentation. Based on your feedback, I just made another pass.
Please feel free to let me know if there is anything specific lacking from the docs, and I will update them in the future.
If you compare say, the Go language specification for an assignment statement [1] to Salt's explanation of its let statement, there is a big difference. Salt's docs lean heavily on "it works like you would expect from other languages" so you have to reason by analogy. A specification shouldn't work that way; it should actually explain the rules for each language construct, without assuming knowledge of other languages.
[1] https://go.dev/ref/spec#Assignment_statements
> [int overflows, etc.] No runtime cost when Z3 can prove it. Otherwise, the compiler emits a safe runtime check as fallback.
Super interesting approach. I see this eventually be integrated into future mainstream languages, though that may take a while. I suspect that the game programming crowd will try to use it first, due to the possibility to prove certain edge cases at compile time and skip the runtime cost. But perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays. I may be too old for these predictions. Cool nonetheless.
Thanks for reading and sharing your thoughts!
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.
---
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...