Formally verified programs often still have bugs. AWS S2N, for example, currently has hundreds of open issues and identified bugs, despite being the subject of a continuous formal verification program.

Bash powers probably hundreds of billions of dollars worth of critical infrastructure...