An interesting idea is what I'd call "proof specificity".
The motivation is to prove that certain classes of bugs
cannot occur. Or, more generally, that certain classes of
behavior cannot occur.
At a very low level there could be a proof that the stack
size is bounded.
A slightly higher level might prove that the implements a
proper protocol such as an FTP copy operation.
Next up might be proving optimizations are correct, for example,
a peephole optimization of register operations. The optimizations
applied during intermediate representations such as loop unrolling
are also interesting.
At the numeric algebra level there are proofs that over/underflow
cannot occur, nor can there be a divide by zero.
At the symbolic level there can be proofs of things like matrix
operations at the algorithm and specification level, independent
of the implementation.
Of course, the holy grail involves proofs that the implementation
implements the specification correctly.
Designing an architecture to support such proof specificity is a
challenge.
Tim