Spectre vulnerabilities violate our fundamental assumptions about programming abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about low-level hardware details such as speculative execution. I will explain the tradeoffs inherent in formal frameworks for Spectre, the complexity of defense tools, and the resulting security guarantees. I will also propose practical choices for developers of analysis and mitigation tools and identify interesting open problems in this area for future work.