(y > 0 && x > INT_MAX - y)
|| (y < 0 && x < INT_MIN - y)
and hope the optimizer turns it back into just checking the result. Or you use -fwrapv to concretize the ISO ambiguity and specify the natural two's complement semantics, checking overflow with the classic Hacker's Delight formula; ((x ^ s) & (y ^ s)) < 0
But the best way is to use the intrinsic __builtin_add_overflow or, depending on compiler support, its C23 standardization via <stdckdint.h> and ckd_add etc.
Fable's napkin estimate of the effort required to produce a passable reference semantics for Postgres, which would involve novel discoveries in denotational semantics of concurrent transactions and so on, might be in the ballpark of 30–60 years of PhD level work.
So realistically I think the only way to validate a Postgres implementation involves differential testing, fuzzing, acceptance test suites, etc. And still you'll have bugs that need to be hammered out the good old fashioned way.