How Amazon built Cedar with automated reasoning

amazon.science

It’s an interesting approach. Using proven correct code written in Dafny and testing it against the same code written in Rust.