Recently replaced by Lean, though. At least in Cedar.

https://github.com/cedar-policy/cedar-spec

https://lean-lang.org

Which is also a Microsoft created language,

https://en.wikipedia.org/wiki/Lean_(proof_assistant)

Yes, Microsoft Research is huge in this space. Z3, Boogie, Corral, Dafny, F*, Lean...

F* seemed promising at one point, but haven't heard much about it in a long time, what happened to it?

Thanks for that. Any idea why? Couldn't find anything by searching their github repo.