内容4：帮助构建验证和程序分析工具的库

在Galois，我们开发了正式的验证工具，这些工具依赖于各种自动求解器来回答数学查询。我们使用的主要求解器称为可满足性模理论(SMT)求解器。这些求解器提供回答诸如“为数学属性找到输入”之类的问题的能力。我们发现这些工具非常有用。已经开发了各种解算器，它们支持不同的问题域，并且在求解复杂的约束系统时非常有效。在其他方面，我们已经使用它们在几秒钟内验证了许多密码算法的正确性，即使输入的数量非常大(2^256个可能的输入甚至更多)。

上周，我们发布了一个名为What4的Haskell库，我们在内部使用它来与不同的SMT解算器交互。What4得名于Why3，这是一个基于OCaml的框架，用于将程序连接到解算器。

What4主要是为了让开发人员更容易构建使用SMT解算器的新验证和编程分析工具而设计的。下面是一个更完整的功能列表，但我们需要一个库，使开发人员可以更容易地以编程方式构造表达式，并将这些表达式发送到求解器进行验证或模型查找。What4利用Haskell强大的类型系统来帮助确保表达式格式良好。What4还包括许多内部表达式简化规则，以保持表达式的简化形式，从而使求解器编码紧凑。

一个活跃的工程师团队，他们每天都在使用它，并支付开发和维护它的费用。

我们邀请您玩What4，在其中建模，打破它，抱怨它，并改进它。我们非常感谢所有的反馈。