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!
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!