[matthavener]

Cryptol does something pretty similar. You implement your functions in Cryptol and then verify them with SAT/SMT solvers, or generative testing. Its less about verifying the C/C++ implementations and more about verifying properties of the algorithms themselves. (Example: https://github.com/GaloisInc/cryptol/blob/master/examples/ZU...)