Towards a Formal Verification of the Lightning Network with TLA+