It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found,

It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found, miners include transactions and signatures are unfalsifiable and not malleable. Roasbeef wanted to do it in TLA+, but I am not sure he will find the time.