1. 12
  1.  

  2. 1

    The work with informal systems on the Agoric smart contracts kernel is my first substantive work with TLA+. Connecting the implementation with the formalization via tests generated by a model checker is my favorite part. We don’t have it running in ci yet, but here’s hoping!