Some unknown benefactor fixed the Peter Buneman Memorial Coffee Machine.
Brian being the Coq expert concluded that he couldn't see any way that dependent types would help us at the moment, so we've pretty much been writing pure OCaml code. At this point we have what appears to be a working tool for checking the score of a particular output image, a renderer for the RNA command language that seems to work, and the DNA execution engine is being debugged. It is hard to conclusively test the RNA renderer until we can begin running the output from Endo's starting DNA. I might write a small high level language to make generating test RNA easier, but not just yet.
However, the hardest part is going to be reverse engineering the DNA they've provided us with.
If none of this makes any sense, you should go check out the ICFP 2007 Programming Contest task description.