@thomasnield just to butt in here, cause I am interested in this too, I came across [this article](
http://pages.cs.wisc.edu/~remzi/Naur.pdf) not long ago and made me think that for new projects that have to prove many things, might be good to collect all the proofs in tests that are not implemented so someone could glance at the project and see what has or has not been done (in conceptual terms)..