[hedora]

The specification includes the semantics of the hardware it runs on, and shows security properties.

Having said that, it is surprisingly easy to get hardware to violate its specifications.

[kjs3]

Which...is not the same thing as 'secure' (although it helps).