It happens... I can think of a couple that bit me in the last 5 years or so. Some of them felt like bugs but were flagged as new features in later releases like this one from 4.4... spent way too long trying to figure out why this worked under 4.4 but not 4.3 and didn't even consider a bug, let alone a feature at the time. I was convinced it was something I did wrong :P

"a. Using ${a[@]} or ${a[*]} with an array without any assigned elements when the nounset option is enabled no longer throws an unbound variable error."

From the anguish of those who try to implement the POSIX shell, I understand that edge cases are far from difficult to find. The Almquist shell (Debian Dash) is cited for not using lex/yacc to implement the parser, and described as untrustworthy.

https://archive.fosdem.org/2018/schedule/event/code_parsing_...

A major goal of this later ADA implementation is readability, in addition to (Windows) performance and ADA's safety.

https://archive.fosdem.org/2019/schedule/event/ada_shell/

Not sure if this counts as "running into an issue", but this bash issue is pretty famous: https://en.wikipedia.org/wiki/Shellshock_(software_bug)

There are design flaws and edge cases in bash though, lots of them come up when trying to automatically show the exit code of the last command and when trying to automatically show whether or not the output of the last command ended in a line ending character.

"I don't think I have ever run into a bash bug or issue."

That is not a statement about a formally verifiable program that I would base a billion-dollar program on.

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...

There are attempts at formal analysis of shell scripts, for eg:

https://colis.irif.fr/ https://github.com/colis-anr/morbig

My point being that whatever other software runs on this thing is far more likely to contain hidden bugs than bash has given its age and widespread distribution. It seems weird to single out bash as opposed to the hundreds of other random packages on any given distro.

Ariane 5 bug was formally verified.

No it really wasn't.