Add new category, program verification.

The inaugural paper in this category describes using Coq to create a
formalised subset of the x86 architecture.