Author: Dmitry Petukhov 2020-05-13 17:02:22
Published on: 2020-05-13T17:02:22+00:00
Ruben Somsen's Succint Atomic Swap (SAS) contract has drawn a lot of interest lately. The author of this post is interested in smart contracts and formal methods to design and implement such contracts. Formal specifications for contracts and machine-checking the properties of these specifications can uncover corner cases that may be difficult to find otherwise. The SAS contract is complex enough to benefit from formal specification and machine checking. The author created a specification in TLA+ based on Ruben's explanation and diagram. The model encoded in the specification can detect the violation of 'no mutual secret knowledge' invariant when one participant can bypass mempool and give the transaction directly to the miner. One transition was unclear, so it was not modeled. The author believes there can be more invariants and temporal properties of the model that can be checked. The specification models the mempool but in a simple way without regards to the fees. An established framework for modeling the behavior in Bitcoin-like blockchain networks would be great in the future. Having a model of mempool-related behavior would help to reason about difficult RBF/CPFP issues. The specification can be found in the author's Github repository. The author welcomes comments, suggestions, and corrections, especially from people experienced in formal methods and TLA+. This is only the author's second finished TLA+ spec and third project using formal methods.
Updated on: 2023-06-14T01:39:29.804968+00:00