I'd love to hear more about your workflow engine, I think the expressiveness of lean and the type system makes it extremely well suited for stuff like that

I do agree that the lack of IO and libs in lean isn't really a drawback when there's a very clear interop path already

I'd love to know more about your experience on this, generally. What have you been doing in Lean? How have you approached this?

Did you have previous experience with formal verification and/or dependent types?