[0xcde4c3db]

Does the formalization have anything that would catch timing side channels, or is that out of scope?

[SolalPirelli]

Out of scope, this work is purely about semantic correctness.

[DoctorOetker]

in theory a provable lack of timing side channels might be possible to formalize, but it would be a tremendous amount of work (from which we will benefit enormously once we do)