[oonwlawx] Multi-precision arithmetic verification

Formally verify the correctness of an implementation of multiple precision arithmetic, for example, GNU MP.  It is a compactly specifiable problem, yet likely very difficult because of complicated algorithms and low level optimization.