TLA+: design, model, document, and verify concurrent systems

I&#x27;ve been learning TLA+ for the past two months, hoping I could use it as a formal language for software design generally and not just for concurrent systems. I&#x27;m enamored with the idea of using math formalisms to describe a state machine.<p>But now that I&#x27;ve gone through Lamport&#x27;s (very charming) video tutorials at OP&#x27;s link and studied some of the specifications at<p><a href="https:&#x2F;&#x2F;github.com&#x2F;tlaplus&#x2F;Examples&#x2F;tree&#x2F;master&#x2F;specifications" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;tlaplus&#x2F;Examples&#x2F;tree&#x2F;master&#x2F;specificatio...</a><p>I&#x27;m less sure now that I can. I&#x27;ll keep plugging away, but if anyone here has any suggestions or offers any alternatives, I&#x27;m all ears.

Raymond Hettinger just have a talk at PyCon an hour ago about formal reasoning and solvers. There’s a lot of polish in the talk, with a whole ReadTheDocs site with runnable Python code with solvers written from scratch. The slides aren’t out yet publicly or privately, but I would highly recommend going through the examples when the PyCon committee releases the information. The way he puts it makes it much less intimidating than I thought it would be.<p>Also Raymond is a very nice guy :D

One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula&#x2F;expression form and code&#x2F;program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.

Interesting. I&#x27;ve worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rust.<p>I wonder if this approach could formally verify systems like seL4.<p>Here&#x27;s an approach to verifying concurrent systems using coq:<p><a href="https:&#x2F;&#x2F;www.sciencedirect.com&#x2F;science&#x2F;article&#x2F;pii&#x2F;S1571066108000765" rel="nofollow">https:&#x2F;&#x2F;www.sciencedirect.com&#x2F;science&#x2F;article&#x2F;pii&#x2F;S157106610...</a>

This keeps getting re-shared periodically on HN. I wonder what&#x27;s HN policy around re-sharing same&#x2F;similar content.