Formal proof of program correctness tends to require that the software's purpose lies in a very narrow, and extremely well-defined problem space. The _Horizon_ software in-question is a general-purpose line-of-business system, which presumably has to react to ever-changing business requirements - that's probably the hardest space to implement formal-methods in - with little benefit for doing-so precisely because requirements change so often.

The places where you do see formal-methods would be in, for example, FADEC for aircraft engines, or an operating system process scheduler.

You don't need a formal proof for the entire system as a whole. You could simply have a formal proof of specific functions of the software. Those functions which will have their data audited, for example.

Correct - but this is a line-of-business application software: so I'm assuming that everything about it is subject to changes. The parts of the system that would be thoroughly spec'd out, QA'd (and maybe do have formal proofs) would be the underlying database system they're using which would be a third-party system like Oracle or Sybase or MS SQL (I just hope they're not using Progress/OpenEdge...).

As it is, I don't know what part of the system is responsible for reporting money stolen by postmasters - the BBC News article is light on technical details. The Register has more details: https://www.theregister.com/2021/04/23/post_office_scandal_f... as does this website focused entirely on the trial: https://www.postofficetrial.com/2019_03_25_archive.html

The bugs are described as being part of the systems' payments processing system (as the Post Office does function as a financial institution, after-all) - but that at least some of the bugs were caused by ad-hoc work on the system (wot, no CI/CD to gatekeep releases?!) so I'm thinking this is just institutional incompetence - let alone a lack of software-engineering processes - so the idea of them implementing formal-methods for proving the system's correctness is laughable.

Formal methods require a comprehensive specification. Usually, if you have a specification comprehensive enough for formal verification, you already have 90% of the benefits, which is why it's (so far) only really useful in safety critical applications with a very small scope. I'm not going to take a huge risk in betting that the postal service didn't have anything resembling a serious spec in this case.

Thats fine, but if they choose to handle money with a joke app, they should eat the losses

That wasn't the issue. Fujitsu, who operated the system, had access to post office branch systems with full access, but this was denied. The postmasters were prosecuted individually without good enough representation. The 2019 judgement is a good read about how the prosecutions happened and how the evidence was presented [1]. Really, formal methods and bugs were not issues, this was a system with humans in and someone decided that some of the humans should be blamed for issues, because the balance of power let them.

[1] https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-...

More than that there was at least one Suicide