Here's a practical example of how Formal Methods can make code faster: AWS's new proven-correct authorization engine is 65% faster (even at p99.9) than the previous version. https://lnkd.in/gVCdurKh Sean says in the talk "we wouldn't have attempted a lot of optimizations we did without this backing of proof". Formal methods allow us to optimize systems more boldly, by removing the risk that optimizations will affect correctness. They also allow our teams to move faster, with lower risk, by building confidence in correctness early on in the software development process.
AWS re:Inforce 2024 - Proving the correctness of AWS authorization (IAM401)
https://www.youtube.com/
Matt Fleming
5mo
Which formal methods were used for AWS authorization?
Databases & math
5mo(somewhat) formal methods helped make MySQL faster, the tools made it easier to contribute a patch that improved performance Long ago when we (at Google) rewrote the InnoDB rw-lock to make it scale on NUMA we shared a SPIN model with the InnoDB team while contributing the code to help them understand the algorithm and reduce concern about bugs. I have used SPIN twice when I was hacking on MySQL. I wish I were able to use it more often. The book is great: https://www.amazon.com/SPIN-Model-Checker-Primer-Reference/dp/0321228626