Witnesses for mathematical software
The concept of "witnesses" or "checkable proofs" is not totally new: as mentioned in the comments, look for the concept of "certificate". Three examples came to mind, there are more (in the comments and elsewhere):


Kurt Mehlhorn described in 1999 a similar problem in computational geometry algorithms (e.g. minor errors in coordinates can yield big errors in the results of some algorithm), solved in a similar way in the library Leda, by insisting that each algorithm produces a "certificate" of its answer in addition of the answer itself.
Demaine, Lopez-Ortiz and Munro in 2000 used the concepts of certificates (they call them "proofs") to show adaptive lower bounds on the computation of the union and intersection (and difference, but this one is trivial) of sorted sets. Don't exclude their work because they did not use certiticates to protect against computing errors: they showed that even though the certificate can be linear in the size of the instance in the worst case, it is often shorter, and hence can be "checked" in sublinear time (given random access to the input as a sorted array or a B-Tree), and in particular in time less than required to compute such a certificate. 
I have been using the concept of certificates on various other problems since seeing Ian Munro presenting their implementation at Alenex 2001, and in particular for permutations (apologies for the shameless plug, another one is coming), where the certificate is shorter in the best case than in the worst or average case, which yields a compressed data structure for permutations. Here again, checking the certificate (i.e. the order) takes at most linear time, less than computing  it (i.e. sorting). 

The concept is not always usefull for error checking: there are problems where checking the certificate takes as much time as producing it (or simply producing the result). Two examples come to mind, one trivial and one complicated, Blum and Kannan (mentioned in the comments) give others.


The certificate for proving that an element is not in an unsorted array of $n$ elements is obtained in $n$ comparisons and checked in the same time.
The certificate for the convex hull in two and three dimensions, if the points are given in random order, takes as much bits to encode as comparisons to compute [FOCS 2009] (other shameless plug).



The library Leda is the most general effort (that I know of) toward making deterministic certificate-producing algorithms the norm in practice. Blum and Kannan's paper is the best effort I saw to make it the norm in theory, but they do show the limits of this approach. 

Hope it helps...