Cedric Fournet uses Lean and said Lean's mathematical library has the abstractions he needs to verify cryptography.

“Jeremy as a user. I knew others would come and pay off. I mean, many people, many of my colleagues that work on cryptography, they say, for example, one of them is a former colleague of mine, Cedric Fournet.”

“He uses Lean now. And he told me, look, the math lib, the Lean mathematical library, have the right abstractions I need for verifying cryptography, right?”