Amazon’s Automated Reasoning Group just published a decade of reflections.

It’s the story of a decade spent proving AWS correct. Their policy engine Zelkova answers 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 in the repo proves the merge algorithm safe in advance.

To the left of CDK is an infra compiler named chant. Zelkova is at the far right, answering questions about existing artifacts.

chant features synthesis as a pure function of the source. Every output value traces to a literal, a constant, or a reference. You ship an artifact that is typed, linted, planned, and signed.

None of chant’s guarantees are a formal proof. Types cannot answer what a policy permits. The output is spec-native JSON though, so Zelkova’s own tooling can check it directly. A wrapper with its own representation would need its own Zelkova.

Now stop and consider how every property chant catches at the keystroke is one less query for Zelkova.

To see a visual of this, check out my blog about flame graphing the leftness of infra tooling.

Read more