bneb-dev

Made updates directly influenced by your input. Please feel free to follow up in Github!

See https://github.com/bneb/lattice/blob/main/docs/deep-dives/z3...

With 92 contributors, I'd bet that The Vera Project is much more mature.

Salt has some different ergonomics and performance goals though, which makes this project unique.

Agree with your overall point. I made some changes to extend the current paradigm a bit: https://github.com/bneb/lattice/blob/main/docs/tutorial/09-c...

---

Invariants aren't always inferred automatically. When they aren't, they can be made explicit for Z3 to check.

At the moment, bubble sort with array-content invariants is fully provable:

  fn bubble_sort(arr: Ptr<i32>, n: i64)
      requires n > 0
      ensures forall i in 0..(n-1) => arr[i] <= arr[i+1]
  {
      for i in 0..n {
          invariant forall k in 0..(i-1) => arr[k] <= arr[k+1];
          // bubble pass
      }
  }

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.

LH seems cool but the syntax would definitely take some getting used to...

It looks like verification is distinct from the compiler.

I'm not sure what the point of bringing up Versus is. Is it https://verus.io/ ? Is it a plug for your own project?

There are several points you made where I think we just fundamentally disagree so I'll decline to engage further at this point.

Hope you have better luck with your candidates and your own projects. I look forward do seeing them on HN down the road!

Looking. I did a huge purge/rewrite of the benchmarks and this might have regressed. Happy to track here or GitHub.

My workflow is to design, then use goal and loop prompts to RALPH a feature. At that point, usually there is a bunch of AI generated code that is generally correct but needs refinement, editing, testing, benchmarking, etc... That human-in-the-loop iterative step is the 'de-slop'. Would you prefer different phrasing, or is the trigger here the use of coding agents?

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.

For loops already worked but might not have been documented correctly. I just shipped the functionality for `while` loops now, auto-infer works for common cases of invariants:

  let mut i = 0;
  while i < 5 {
    arr[i] = val;
    i += 1;
  }

(Works with `<`, `<=`, `i += 1`, and `i = i + 1` via the same mechanism as for-loop induction variables.)

Complex loops (`while i + j < n`, `while p.addr() != 0`) require syntax that I have slopped together an explicit `invariant` keyword that I am not 100% happy with, but will refine later. Z3 checks base case + inductive step via Hoare logic and reports counterexamples on failure.

---

RE: "gnarliest invariant"

`ensures(result != 0)` on the SYN cookie in the kernel contract for the OS project in the monorepo.

Not sure what tone you're going for, but can you expound on what you mean by 'ai-created'?

What gives you that impression?

Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?

It was a design decision. I chose Arenas instead.

The designed arena allocation is both faster and more predictable than GC. The trade-off is that you have to think about memory regions, but you never pay a GC pause.

This is being made by one person as a side project (not done during core working hours)

Ah, the issue is that I don't like that syntax: Salt is macro free, and doesn't need assert statements, etc... These are stylistic but I am assuming that under the hood things look quite similar.

I put an effort in to de-slop the project wherever I can. If you've noticed anything specific, I'd kindly request that you open an issue on Github or respond here with your findings so that I might correct them in the future.

Thanks for taking an in-depth look at Salt.

Haven't heard of Venus (the programming language), but it sounds interesting. I'm curious to know what you mean by verified?

Do you happen to know if Venus has a Result type with canonical error codes, pipes, and other ergonomics?

Does it have C parity performance?

Thanks, I restructured that doc and will work on it moving forward.

SPARK seems interesting. Any ideas how it compares to Salt?

- C performance? - Generics? - Syntax ergonomics?

Thanks for sharing!

Thanks for reading and sharing your thoughts!

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.

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