The Succint Atomic Swap contract presented by Ruben Somsen recently has drawn much interest.
I personally am interested in the smart contracts realizeable in the UTXO model, and also interested in applying formal methods to the design and implementation of such contracts. I think that having formal specifications for the contracts and to be able to machine-check the properties of these specifications is very valuable, as it can uncover the corner cases that might be difficult to uncover otherwise. The SAS contract is complex enough that it may benefit from formal specification and machine checking. I created a specification in TLA+  specification language based on the explanation and the diagram given by Ruben. The checking of the model encoded in the specification can successfully detect the violation of 'no mutual secret knowledge' invariant when one of the participant can bypass mempool and give the transaction directly to the miner (this problem was pointed out by ZmnSCPxj in the original SAS thread ) There's one transition that was unclear how to model, though: I did not understand what the destination of Alice&Bob cooperative spend of refund_tx#1 will be, so this transition is not modelled. I believe there can be more invariants and temporal properties of the model that can be checked. At the moment the temporal properties checking does not work, as I didn't master TLA+ enough yet. The safety invariants checking should work fine, though, but more work needed to devise and add the invariants. In the future, it would be great to have an established framework for modelling of the behavior in Bitcoin-like blockchain networks. In particular, having a model of mempool-related behavior would help to reason about difficult RBF/CPFP issues. The specification I present models the mempool, but in a simple way, without regards to the fees. The specification can be found in this github repository: https://github.com/dgpv/SASwap_TLAplus_spec There could be mistakes or omissions in the specified model, I hope that public review can help find these. It would be great to receive comments, suggestions and corrections, especially from people experienced in formal methods and TLA+, as this is only my second finished TLA+ spec and only my third project using formal methods (I created bitcoin transaction deserialization code in Ada/SPARK before that ). Please use the github issues or off-list mail to discuss if the matter is not interesting to the general bitcoin-dev list audience.  https://lamport.azurewebsites.net/tla/tla.html  https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May/017846.html  https://github.com/dgpv/spark-bitcoin-transaction-example _______________________________________________ bitcoin-dev mailing list firstname.lastname@example.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev