I'm not familiar with formal verification, so forgive me. Could something like TLA+ be used to inch yourself towards a verifiable spec? Although you are moving the goalpost, the hope is that eventually your spec is so simple that it is "obvious" that it is correct?