lattice

s (4 iterations × 2), all proven at compile time, outputting Z3: 8/8 checks proven (100%), 0 deferred to runtime. And insertion sort is partially provable: This starts with the same `forall` invariant structure. After the base case, the outer for-loop inductive step is wired but the inner while-loop's trip count depends on the data which can't be determined statically for which indices were modified, so the frame axioms can't fully constrain the array state. This would require splitting on the case for the while condition, which is future work, and wasn't part of my v1.0.0 plans.

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...