I won a copy of the book Hacker's Delight from John Regehr for my entry in his nibble sort contest earlier this year.
In that thread I had heard about the CBMC Bounded Model Checking software, and it gave me the idea to combine the two: a project to take implementations of the algorithms from Hacker's Delight and prove the algorithms' properties with CBMC.
I have a modest start on github, which I am calling "Proven Delights":
All older entries
Website Copyright © 2004-2018 Jeff Epler