Author: Dmitry Petukhov 2020-06-01 11:38:54
Published on: 2020-06-01T11:38:54+00:00
The author has completed the specification of the Succint Atomic Swap contract in TLA+. The specification covers all relevant behaviors of the participants and even has an option to enable 'non-rational' behavior, so that transactions punishing bad behavior can be utilized. The model is capable of exhaustively checking safety properties, such as no participant being able to take both coins, unless explicitly specified circumstances exist, and temporal properties, such as the contract always ending up in an explicitly specified 'finished' state. Additionally, the model can show hyperproperties, such as which transactions can ever be confirmed in at least one execution path, max/min/avg values for various stats, etc. However, automatic checking of hyperproperties is not yet available. The model has some limitations, like only having one miner and not modeling fees and mempool priorities. Despite these limitations, the author believes that TLA+ is a suitable tool for specifying and checking smart contract specifications. The goal of creating this specification was to evaluate the suitability of TLA+ for modeling smart contracts in UTXO-based blockchain systems. The author hopes that this specification can be used as a basis for other contracts and increase interest in using formal methods in this area.The author did not make specific effort to factor out generic logic into separate modules, but expects to further understand what is really generic and what should lay with concrete contract logic through the design and analysis of various contract specifications. Lastly, thanks were given to Ruben Somsen for designing the contract and providing helpful descriptions and diagrams that made it possible to create this formal specification.
Updated on: 2023-05-20T23:21:34.062306+00:00