Comment by IshKebab
13 hours ago
Interesting... But I don't think formal software verification is going to be the answer (is that what this is? Kind of unclear.)
It's too difficult and doesn't scale well to many real world programs - how do you formally verify Facebook?
We'll probably be stuck with normal testing and at least skimming code for a while.
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.