Software that runs critical infrastructure (or could cause injury or death if it malfunctioned) should be required to use formal methods and that certainly would include everything to make it run also used such formal methods. (From the OS to shared libraries and even the compilers)

"Microsoft and the device manufacturer and installer exclude all implied warranties and conditions, including those of merchantability, fitness for a particular purpose, and non-infringement."

You'd have to outlaw that or breed a more discerning consumer. One way to do that would be to blame the company using it, which would make them take more care in what they choose to use.

It just gets broad and vague after a point. Can the software that schedules trains use Linux or MySQL? People could die if it puts two trains on the same track. Note that GP never mentioned safety either. Just being hacked.

But yes I'd hope that anything bespoke should be covered under a contractual agreement with SLAs and penalties.

The software that schedules trains can do what it likes, because there are several, independent safety layers below it: the signaling system itself, and the software and hardware locks within the signaling system, and formal methods usedto prove their integrity.

Any signaling failure will fail safe (all trains stop).

Any trusted actor (controller, train driver, sometimes passengers etc) can also stop part or all of the system. (On many European railways, if the driver sees a problem, like a car crashed into the railway, they press a red button and all trains in that region are halted.)