[jnash]

Can you elaborate a bit more on the kind of projects you have used Coq (and other tools) to prove correct? I am very much interested in moving in that direction career wise.