QuickCheck
Yesterday I had to prove that a certain algorithm (for a variation on lambda-lifting) was correct. I wasn't really sure that it was correct, so I took some time and coded it up in Haskell, then picked up enough knowledge of QuickCheck (the manual is more helpful than that raw interface file, but it uses HTML frames to crush your spirit) to write some randomized tests for the algorithm.
At first it caught some good bugs. Then it started succeeding on 100 random tests every time I ran it, so I feel reasonably certain that my algorithm is correct. I played around with the test-data generator to make sure it was generating terms that were deep enough and rich enough & to make sure that it never diverges, creating arbitrarily large terms. QuickCheck is reasonably nice this way.
So here's the Haskell code for my lambda-lifting algorithm, together with the QuickCheck tests (at the bottom). Note that there are some funny things in the syntax that aren't explained; they'll have to stay unexplained until I get done with the actual research I'm doing! Any day now...