prang Wichmann-Hill Pseudo-Random Number generator Implementations in C and SPARK Ada to illustrate capabilities of various verification tools.