A billion proofs a day

Amazon's Automated Reasoning Group published a decade of reflections on proving AWS correct, highlighting that its policy engine Zelkova answers a billion SMT queries a day about what policies permit. The group's work includes a machine-checked Alloy model in the AWS CDK repo that proves the risky statement merge algorithm safe in advance.

Amazon’s Automated Reasoning Group just published a decade of reflections https://www.amazon.science/blog/a-decade-of-mathematical-certainty-reflections-on-the-automated-reasoning-group . It’s the story of a decade spent proving AWS correct. Their policy engine Zelkova answers a billion SMT queries a day https://www.amazon.science/blog/a-billion-smt-queries-a-day about what policies permit. Every one of these queries happens after the artifact exists. The queries are against normal JSON that nothing upstream cleans up or constrains. CDK has a miniature version of this. It runs a risky statement merge at synth, so a machine-checked Alloy model https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-lib/aws-iam/docs/policy-merging.als in the repo proves the merge algorithm safe in advance.