Since the disclosure of Spectre attacks in 2018, both academia and industry have made considerable efforts to defend against all variants of transient execution attacks, the class of attacks to which Spectre belongs to. The first part of this presentation will be dedicated to discovering how these attacks change the way we reason about threat models in security. The second part of the presentation will introduce a new generic formal processor model - called ProSpeCT - to prevent transient execution attacks by construction. ProSpeCT has also been implemented on top of an open-source RISC-V processor and will be presented in Usenix Security 23 in a joint work with Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, and Frank Piessens.