Description: TRAC is a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, TRAC can specify the coordination of the participants of a distributed protocol for instance an execution model akin blockchain smart contracts (SCs). TRAC relies on a notion of well-formedness to rule out meaningless or problematic specifications shown to be suitable on several case studies borrowed from the smart contracts domain.

Developed at: GSSI, NOVA

Contacts: emilio.tuosto@gssi.it,  aravara@fct.unl.pt

Available at: https://github.com/loctet/TRAC