I'm not 100% convinced that "plugging memory error holes" was right at the compiler level.

Currently building out clr, which uses a heuristic (not formal verification) method for checking soundness of zig code, using ~"refinement types". In principle one could build a more formal version of what I'm doing.

https://github.com/ityonemo/clr