Citizen Lab found an actively exploited zero-click vulnerability being used to deliver NSO Group’s Pegasus mercenary spyware while checking the device of an individual employed by a Washington DC-based civil society organization with international offices. We refer to the exploit chain as BLASTPASS. The exploit chain was capable of compromising iPhones running the latest version of iOS (16.6) without any interaction from the victim.
Formal Verification doesn’t guarantee that the code is free of vulnerability, it just increases confidence in its security. It’s never perfect.