It's a nice accomplishment, but even the article footnotes note that getting the definitions right for the paper was as important as verifying the actual proofs. And a proof assistant cannot fully verify your definitions, so these checks are still largely left to human scrutiny.
Just to clarify, Bose et al.'s paper was incorrect due to an incorrect definition of Stirling numbers of the second kind (some of their expressions used the wrong exponents). In our certified work, in light of this error, we ended up deriving the expression for Stirling numbers of the second kind from first principles[1], eliding it as a source of errors. As such, the main definition that needs to be human-verified in our work is the actual implementation of the Bloomfilter[2], which is fairly simple and easy to check as being correct.
