Tech Talk - Modelling the Agoric smart contract kernel using TLA+

Agoric is a smart contract platform built for Javascript. In October 2021, Andrey Kupriyanov and I presented a talk on modelling parts of the platform in TLA+. The platform has several protocol layers including a remote promise resolution layer and local and distributed garbage collectors.

Links

• Youtube
• Model of local garbage collector protocol with a byzantine process
• Model of remote garbage collector protocol with correct processes