@krismicinski @kha @markusde in a way, yes, but not in the full Iris-style generality. We think of Lean as an IR to embed sound domain-specific verifiers with a good amount of proof automation and lightweight validation.