1. 18
  1.  

  2. 3

    The companion book also looks pretty nice - https://www.stateright.rs/

    1. 1

      Cloud service providers like AWS and Azure leverage verification software such as the TLA+ model checker to achieve the same goal, but whereas those solutions typically verify a high level system design, Stateright is able to verify the underlying system implementation in addition to the design (along with providing other unique benefits explained in the “Comparison with TLA+” chapter).

      This seems really promising, though I haven’t delved into the programming model yet. The TLA+ Comparison page looks interesting too

      1. 1

        This seems really promising, though I haven’t delved into the programming model yet. The TLA+ Comparison page looks interesting too

        I asked him about it over on the Orange Site, and he said it works by tying all of the actors to a test orchestrator. So they can run in production, but they can also run in a special “test” mode which (I think?) exposes all of the things they can do, and then the model checker can exhaustively explore the behavior space.