[ryao]

Another contributor who is watching this more closely informed me that the issue appears to predate Oracle’s acquisition of Sun. While this is bad, it at least suggests that this bug is very rare.

The code has never been formally verified, so there was always a possibility of such a bug existing. Without formal verification, it is possible that more such bugs will be found. I should add that there is no formally verified production ready storage stack, so not using ZFS would not eliminate the risk of hitting bugs like this. :/

[steponlego]

Formal verification seems more appropriate for finished software not undergoing development or feature changes. It's the last step before software is set permanently in stone, unchanging, forever.