> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.

Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.

▲

Ericson2314 2 hours ago | parent [-]

We can formally verify the Verilog or equivalent too.

	▲	breakwaterlabs 10 minutes ago \| parent [-]
		You cannot formally verify heat-induced transistor stability issues, solar radiation, next-cell state change caused by EMF from adjacent cells (rowhammer).... And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks.... It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.