Cryptol

Cryptol

简介

Cryptol 是用于在 C 和 VHDL 中设计安全密码系统的加密语言，使用 Haskell 语言编写。

功能

Cryptol 第2版解释器包括一个 :check 命令，该命令针对随机生成的测试向量（test vectors）测试用 Cryptol 编写的谓词（类似 QuickCheck 风格）。还有一个 :prove 命令，用于调用 SMT 求解器，如 Yices Z3 或 CVC4 以证明所有可能的输入的谓词。

项目

• Cryptol @ GitHub

文档

• Verified Cryptographic Code for Everybody

图集

• 

  Cryptol REPL

链接

• Cryptol官网
• Galois, Inc.