TLA+ Source Files for Paper "Model Checking the Security of the Lightning Network"

Overview of files The script download-and-run-tlc.sh downloads the model checker TLC and runs TLC in model checking mode for the scenarios that are listed in Table I and Table II in the paper and in simulation mode for a model for each refinement step.

For each of the main specifications shown in Figure 4, there is a file containing the definition of the specification (see below "Specifications").

Additionally, there are specifications named in the form SpecificationXtoY that extend one of the main specifications with auxiliary variables to allow for defining a refinement mapping from specification X to specification Y.