imagine having 'proof coverage' in a build process. i.e. highlight a bit of TeX that is proved by some series of formal statements. or some idea like this anyway.
obviously, don't want to have to actually use coq or similar; but maybe there is something close to this idea that is still nice. i.e. 'this document has 85% proof coverage'.