I've also seen situations where a customer reports a bug, the fix breaks some regression, and the updated behavior to work around the fix breaking the regressions turns into an undocumented feature.

The same basically holds for proofs in the absence of coherent global correctness criteria like, say, confluence and normalization for a lambda calculus, or soundness and completeness for a logic.

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.