Some parts of this are true, but bringing up z3 is kind of a random tangent without any actual knowledge to be shared behind it.

formal modeling and verification doesn't become 100% magically useless just because you can't assert semantic correspondence automatically. one would expect a champion of understanding to understand this.

way to take issue with credibility from a blatant sockpuppet account by the way. like, really dude?