Experimented a bit with Monadic Cryptography in Lean. I feel like Lean is going to be too cumbersome for doing actual Cryptography here. Really, any proof assistant is too annoying. Designing a custom language for things like this seems more promising. The Embedded DSL thing is just likely too verbose, with all the monadic reasoning cruft you’ll need. I can already see the endless toil in proving that some effects commute, etc.