Review TLA* specification

[shielded-nate]

HT to @oxarbitrage for providing this: https://github.com/oxarbitrage/crosslink2 ! 🛡️

We haven't looked at it yet, and I wanted to file this ticket to track this specification. This could be quite helpful, even without a toolchain, just do discover different interpretations of the Crosslink2 paper.

I'm unaware of TLA*. Is this the right starting point? https://github.com/tlaplus

[oxarbitrage]

The references i found more useful for tla+ and pluscal are:

https://lamport.azurewebsites.net/tla/book.html

https://learntla.com/index.html

[shielded-nate]

Ok, as noted on today's Arborist call, an important step in the formal verification space is to get a dispersion of interested parties into a call together. (This is tangential to this ticket.)

[oxarbitrage]

Related: daira/tfl-book#165

I am happy to create an agenda and facilitate the call if you want.

[shielded-nate]

I pinged you on signal about setting up a meeting.