[nanolith]

There is a third category of memory and other software safety mechanisms: model checking. While it does involve compiling software to a different target -- typically an SMT solver -- it is not a compile-time mechanism like in Rust.

Kani is a model checker for Rust, and CBMC is a model checker for C. I'm not aware of one (yet!) for Zig, but it would not be difficult to build a port. Both Kani and CBMC compile down to goto-c, which is then converted to formulas in an SMT solver.

[dnautics]

There isn't a real one yet, but to scratch an itch I tried to build one for Zig. It's not complete nor do I have plans to complete it. https://github.com/ityonemo/clr

If zig locks down the AIR (intermediate representation at the function level) it would be ideal for running model checking of various sorts. Just by looking at AIR I found it possible to:

- identify stack pointer leakage

- basic borrow checking

- detect memory leaks

- assign units to variables and track when units are incompatible

[DrNosferatu]

Any good primers on SMT solvers?

[nanolith]

Start with this.

https://smt.st/SAT_SMT_by_example.pdf

The algorithms behind SAT / SMT are actually pretty straight-forward. One of these days, I'll get around to publishing an article to demystify them.