See also my comments here - https://news.ycombinator.com/item?id=50365641 and https://news.ycombinator.com/item?id=50375318 (this one explains how static analysis works which is the confusion i see above).
The idea of a "proof" which is what Symbolic Execution by a Static Analyzer does is different on both sides of the above isomorphism. You cannot mix them indiscriminately. This is because C++ does not have a typing theory (in the sense of lambda calculus derivatives) but simply maps types to sets. Hence one cannot do "Type-Driven Design" natively like a lambda calculus-based language even though you can do aspects of it via explicit programming techniques (eg. see "Functional Programming in C++ by Ivan Cukic").
That is the reason i suspect contracts in C++ moved away from the original focus on static analysis to managed runtime checks + some static analysis. C++26 contracts are firmly in the Set Theory/Predicate Calculus camp and are not integrated into the Type System.
We need an augmentation of the C++ type system and then a narrowing so we can end up with something like Ada-SPARK (call it "Safe C++"/"Profiles"/whatever).
I didn't mean to claim type systems/static analysis in general are not mathematically sound, but that bolting "static analysis" on to something obviously mathematically unsound doesn't give you actual types. A language allowing you to express new invariants and runtime guarantees it can't enforce (not just because they're unimplemented, but because what an implementation would need is not even expressible) is more inconsistent than one where you can't make unenforceable claims
You basically need a complete LEAN-style predicate calculus to generalize guarantees on runtime invariants through compile-time analysis. You are making claims on the interior structure of data that is defined by how many bits of information it encodes, including at the boundary where provenance ends (the arguments passed into your binary are all basically just multiples of 4/8byte enums, ints, strings, or floats), where you'd also need to be able to check/enforce that the data has particular properties, otherwise all you did was introduce more ways to do UB
C++ has nothing close to this in place and it's in fact quite a different claim that any particular invariant is obviously statically verifiable, or that a large class of assertions would be very easy to prove statically, than the claim it would be fine to only catch "most" or even "many" type assertions statically and just handle the rest at runtime.
It's like saying "well 2 + 5 obviously < 10 and most static checks are obvious, so it's better to at least handle that even if we can't statically prove which particular subset of N have 2^N % 10 = N and just check the really hard stuff at runtime". Because that means you have to ask whether any runtime failure is some emergent/adversarially difficult problem from number theory, but at least you can catch all the easy stuff you would have caught anyway