[dranov]

Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean.

https://aws.amazon.com/blogs/opensource/lean-into-verified-s...

[muraiki]

Oh whoops, thank you for the correction! I didn't realize that.