Názor k článku Procesory Intel mají vážnou hardwarovou chybu, záplata výrazně snižuje výkon od Sten - Halting problem říká, že nemůžete jednoznačně rozhodnout, jestli...

Halting problem říká, že nemůžete jednoznačně rozhodnout, jestli daný algoritmus skončí. To ale pro formální verifikaci nepotřebujete, pro formální verifikaci budete vyžadovat důkaz, že algoritmus musí skončit, a pokud to dokázat nejde (tedy i pokud to nejde rozhodnout), tak není verifikovaný. To znamená, že formální verifikace má povoleny false negatives (bezpečný kód neprojde), ale nikdy false positives (nebezpečný kód projde).