Can this feature proposal be lifted from a best-effort base to be reproducible?

Something like preconditions contracts, which have to be provably be true at compile-time.

Can there be hints to guide the compiler to a deterministic proof?

 
We could at least specify that if the condition is a constant expression, the assertion behaves correctly instead of being best-effort. Anything past that would seemingly require us to standardize a bunch of control flow and data flow analysis, and I don't think anyone wants to do that just for the sake of this assertion.

I think the target audience for this feature is aware that it's playing Russian Roulette with compiler errors, and should probably never be used in large production code bases that compile with more than one compiler, or at least not with default build flags. Making the feature even slightly more predictable comes with great effort, and I don't think it would meaningfully impact who would or wouldn't use the feature.