Is EC2 real-world enough? From June:

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-corecryp...

Similar from Microsoft, from July:

https://www.microsoft.com/en-us/research/blog/verifying-rust...

Funny you say that while OpenAI and rest of the world rely on Lean and other formal systems to power through (or sometime brute force) math problems.