i've seen static analyzers catch many ub patterns, but guaranteeing zero ub needs whole‑program analysis that blows up compile time and still produces false positives that drown developers

Yes, it's pretty much impossible to prove anything about arbitrary programs.

However if you are willing to restrict what programs you allow, you can make guarantees possible.

Silly example: if you compile valid (safe) Rust programs to C, you know that the resulting code will not invalidate Rust's borrowing rules by construction; and in principle you could try to establish this guarantee just from the C code alone, never having seen the Rust original.

However, you still wouldn't be able to have an algorithm that tells you for any arbitrary C code whether it has these problems or not.