aws-cdk

ct in Root.*contents } // Every fs object is in at most one directory assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents } I initially thought these model checking languages were purely academic in nature. But then a curious problem came up when I was working at AWS where folks were complaining that IAM policies generated by our library were sometimes growing to be too large in size (usually the limit was a few KB) - often due to redundant statements. To solve this, a coworker implemented some code for merging IAM policies -- though the merging processe wasn't trivial because IAM policies can have both "Resources" and "NotResources", "Actions" and "NotActions", "Principals" and "NotPrincipals" etc. So to prove the algorithm was correct, he wrote up a short Alloy specification[1] (roughly mapping to the library code) that proved if two policy statements were merged, it wouldn't change the security posture. As a new engineer to the team, I'll just say that it blew my mind that this was possible -- actually using proofs to achieve goals in industry. Needless to say, I'm curious to dive into Quint's differences and what kinds of models/specifications it excels with. [1] https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-li...