Cryptol

http://www.galois.com/technology/communications_security/cryptol
> Cryptol is a language for writing specifications for cryptographic algorithms.
> It is also a tool set for producing high-assurance, efficient implementations
> in VHDL, C, and Haskell. The Cryptol tools include the ability to equivalence
> check the reference specification against an implementation, whether or
> not it was compiled from the specifications.

言語にHaskellが入っている点に超期待．非商用に限り，トライアルできるようです．
for Linux(rpm), MacOS10.4/5(tar.gz), Windows(msi)

http://www.galois.com/files/Cryptol/Cryptol_casestudy.pdf
> DSLs (domain specific languages) allow subject-matter experts
> to design solutions in using familiar concepts and constructs.
> Cryptol is an example of a DSL for expressing cryptographic
> algorithms. The capabilities include:
> - Create a reference specification and associated formal model.
> - Compile the implementation for multiple targets:
> C/C++, Haskell, and VHDL/Verilog are currently supported.

もうゴリゴリ組み込み用コード書かないからなぁ．