Reading that, the execution is now deterministic but the soundness is still probabilistic and <100%, no? Unless I'm reading it wrong.