Comment by mlindner

You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.