I don't understand why you got downvoted. Even if GP meant that a CPU that is advertised as formally verified must be deterministic... the devil is in the details, and any number of bugs and undocumented features, including vulnerabilities and backdoors, can hide in a formally verified CPU that has billions of transistors.

Even if it seems deterministic now, there's no guarantee it won't become non deterministic in the future. https://ieeexplore.ieee.org/document/7546493

This is a very valid point, and there is even anecdotal evidence that operations we expect to be deterministic may not always be so.[1] Just because ADD works as documented in most scenarios doesn't mean we can verify that it will always work as documented in every scenario.

[1]: https://techreport.com/review/17732/intel-graphics-drivers-e...