Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
> it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x)
And it does not matter, since the point of formal verification is to help taking those issues into account.
Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.