You're right. It just seems as though it should be self-evident. Especially to those sophisticated enough to understand and employ formal verification.
Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.