One angle on this I'm particularly excited about is the formal methods/automated reasoning work the team did on Cedar: https://www.amazon.science/blog/how-we-built-cedar-with-auto...

"We want to assure developers that Cedar’s authorization decisions will be correct. To provide that assurance, we follow a two-part process we call verification-guided development when we’re working on Cedar. First, we use automated reasoning to prove important correctness properties about formal models of Cedar’s components. Second, we use differential random testing to show that the models match the production code."