This is a cool project, but it doesn’t address my original issue with Zig, which is that the language’s semantics is not even specified. That is, we cannot define what a “memory safe Zig program is” as we cannot even define what a Zig program is! (Unless you define the semantics of a Zig program in terms of the implementation/translation to IR, which is fragile / bad.)

Second, I would be surprised if the static analyses in the tool are precise enough for real-world Zig programs. For example, it is undecidable to determine whether a function “takes ownership” of an argument pointer. In particular, if you want to avoid false negatives, the “free after transfer” case needs to be conservative, but then you almost certainly will flag false positives.