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).

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.

You can't prove it in Rust either.