AWS says that when code has a good set of formal verification they can be as aggressive as possible in performance optimization without having to worry they are

AWS says that when code has a good set of formal verification they can be as aggressive as possible in performance optimization without having to worry they are breaking the logic of the code. This helped them double the performance of the IAM ACL evaluation code.