Possible and (relatively) easy. We write the formal definition of the function in Cryptol, and use the Cryptol toolset to compare it to our implementation. Cr

Possible and (relatively) easy. We write the formal definition of the function in Cryptol, and use the Cryptol toolset to compare it to our implementation. Cryptol[1] has the amazing ability to verify implementation equivalence between [a large class of] functions written in Cryptol, C, Java, Assembly or VHDL (as far as I recall). Of course this class of functions is not Turing Complete, but it's good enough to verify that two implementations of SHA256 or AES are mathematically identical. The way Cryptol does this is really interesting: they compile the functions to a logic circuit, and use a SAT solver to prove that the circuit (f(x) == g(x)) always outputs T. [1] http://www.cryptol.net/ http://www.cryptol.net/, an open source functional language made for Crypto R&D and communication, designed by Galois Inc. on commission from the NSA