The Software Analysis Workbench (SAW) provides the ability to extract formal models from programs written in C (via LLVM) or Java, and analyze them using a variety of automated reasoning tools. SAW allows you to verify that an extracted formal model matches a specification of the same functions written in Cryptol. We have plans to add additional languages and back-ends to SAW. See the contact information on the SAW page if you have any further questions.