Memory safety prover/SPARK for Zig?

Is there any sort of memory safety prover for zig? Similar to SPARK for Ada

No - but there are interesting proofs-of-concept and linters and strategies that I’m fairly convinced will lead there in time.