Formal verification of not having such fatal bugs would allow a real-time system without reliance of backups to not screw up, but still of course having logs/ro

Formal verification of not having such fatal bugs would allow a real-time system without reliance of backups to not screw up, but still of course having logs/rollbacks for (human) input actions to cope with mistakes. It's just that production software essentially never used formal verification to a sufficient extend.