From what I'm seeing here, all the individual things that were done _were_ correct. It just so happens that the system was setup with rules that allow for this type of thing. A probably correct program would not have helped here.

The problem is that you can't predict ahead of time every use case.

That's why today's financial system has the ability to manually revert back to a previous state if something gets wrong e.g. undo transactions, government bailouts etc.

Hey Matt! There is some interesting work done in this area. For example https://reach.sh/ lets you write formally verified smart contracts.

I guess this is helpful with some classes of bugs. But I'm not sure it would with most. For example it is unclear if it would have caught this problem since (from the vague description!) it appears it would have needed some economic modelling to catch.