Salt v1.0.0 – a systems language with Z3 theorem proving in the compiler

Salt is a new systems programming language (v1.0.0 just released) that bakes formal verification directly into the compiler using Z3, a famous theorem prover from Microsoft Research. This means the compiler doesn't just check types or memory safety — it can mathematically prove that your code meets certain logical specifications (e.g., "this index is always in bounds" or "this function always returns a positive integer") at compile time. For readers: "Systems language" puts it in the same family as C, Rust, Zig — languages used for operating systems, embedded devices, and performance-critical software. Z3 is the same engine used by many static analysis tools and bug finders; having it built into the compiler is unusual and ambitious. The project appears to be a research-adjacent language rather than a production tool (no major backers like Rust has Mozilla/Google), and the timeline for maturity is unclear.