Concurrent and distributed programs

Stream: Program verification

[Gerard Finol]

Can Lean be used to model programs and systems, especially concurrent and distributed ones?

In case it can be used, where can I find some documentation or guides about that?

[Ethan Barry]

I've tinkered with TLA+ a bit, and I'm learning Lean now, so I can probably provide an answer to the can/should question...

AFAICT, Lean can model systems as mathematical entities. But, if you're verifying software on a limited schedule/budget, working in a model checker like TLA+ is probably more efficient than formalizing your entire system in Lean and then proving properties.

I found a HN comment that basically says this ^^^ from a Ph.D. in formal methods here, and the Lean website has this related slide deck. Hope that helps somewhat...

[Bas Spitters]

What are you looking for more precisely? There's been a lot of work on modelling concurrent programs using program logics (https://iris-project.org/). There's been an initiative in replicating this in lean, but most of the code is in Coq/roqc ATM.
There's also quite a bit of work on modelling distributed systems (again in Coq/roqc). E.g. verification of raft or Nakamoto consensus. Similar ideas can be applied in lean.

[Karl Palmskog]

see also previous discussion here: #Program verification > Algorithms in Lean @ 💬