Is EC2 real-world enough? From June: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/

Is EC2 real-world enough? From June: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/ https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng... And for the PQ parts of Apple's crypto libraries, from May: https://security.apple.com/blog/formal-verification-corecrypto/ https://security.apple.com/blog/formal-verification-corecryp... Similar from Microsoft, from July: https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/ https://www.microsoft.com/en-us/research/blog/verifying-rust...