alt Hacker News> if the software you were running was advertised as formally verified as free of bugs.
Nobody should be advertising that. Even ignoring the possibility of bugs in the runtime, there could also be bugs in the verifier and bugs or omissions in the specification. Formally verified never means guaranteed to be free of bugs.
As quoted in the article itself, please take it up with the chief architect of the Lean FRO:
> ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.
> Not tested. Proved. For every possible input. lean-zip