New paper! "Verifying an Efficient Algorithm for Computing Bernoulli Numbers" As a case study, I took the most efficient algorithm known for computing Bernoulli numbers and verified the hell out of it, and then Peter Lammich refined it all the way down to efficient LLVM code. Not quite as fast as the original unverified C++ code, but that's not because verification is hard but rather because I'm bad at optimising x86 assembly at that level. 😅 Will be presented at ITP in Reykjavík next week. https://doi.org/10.4230/LIPIcs.ITP.2025.35