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.
source & further reading
lex00.github.io — original article
De-stink: remove claudisms without LLMs, only copy paste
Anthropic reached the same list
Queryable Infrastructure