As Zig promises "not hidden allocation", I assume you can build your allocator in Rust and then use it for all memory allocation in Zig.

A function that doesn't allocate doesn't mean it's safe. (Indeed if anything the opposite is more likely - copying is safe, if slow, writing to something that was passed in tends to be what breaks).

You can't prove it in Rust either.

formalized subsets of x86 assembly exist. Coq can be used as a macro assembler. tools to work with llvm ir exist, x86 can be raised up to llvm ir and proved, kinda bad way tho.