Why3

一个 Rust 库，提供了 Creusot 验证器使用的 Why3 AST 及其相关的 pretty 打印器。该库支持三种 why3 输入格式：WhyML (.mlw), coma (.coma) 和 Coma (.coma).

目前，Why3 的核心 Exp 类型因作为 creusot 的衍生品而积累了大量技术债务。我希望逐步清理这些问题，但如果您计划在一个项目中使用 why3，请与我联系，以便我可以重新安排优先级。