I heard a talk by a group that is doing exactly this. They built their own language to model crypto primitives, and machine check that a java or c implementation satisfies the specification. It is neat stuff, but unfortunately their system can't model timing differences, which is an important part of crypto implementation.