I’ve been vibe coding a lot of Lean this year.

What i found is that it is amazing once you determine and the invariants that are essential to the guarantees you want to keep.

I built my own formally verified workflow engine, it was easy but mostly because i already knew the pitfalls and the foundational pillars of Cadence and Temporal.

Also, it doesnt seem like common knowledge, but you can export libraries that compile to C from lean. With them you do get performant code that that has been verified and easily call them as C bindings from elsewhere.

Lean itself does not have a good IO stack in general but its good enough for small projects.

There is a caveat to exporting libs or native_decide in general. Once you export into C, ABI its now outside of the scope of the Lean kernel which means that bugs can creep in from the compiler itself.

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?