[Cladode]

That's an interesting question: can Lean be implemented in Lean's dependent type theory.

I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.

[agentultra]

That sounds like it could be a lot of fun! Good luck. :)