# A billion proofs a day

> Source: <https://lex00.github.io/posts/a-billion-proofs-a-day/>
> Published: 2026-08-15 00:00:00+00:00

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.