Microsoft 开源 Z3 在线指南
Online Z3 Guide
Microsoft 推出了全新的 Online Z3 Guide，为开发者提供了一套完整的 Z3 求解器学习资源。这套指南不仅包含 SMTLIB 教程和 JavaScript 编程示例，还内置了可交互的 Playground 环境，让开发者能直接在浏览器中编写和测试代码。从 Python 编程到 API 文档，再到 GitHub 源码，资源一应俱全。无论你是刚接触形式化验证的新手，还是希望提升 Z3 使用技巧的资深工程师，这个在线指南都能帮助你快速上手，探索 SMT 求解器的强大能力。
Z3 Guide 提供了从 SMTLIB 教程到 JavaScript 编程示例的完整学习路径。
HN 评论区
14- olooney
我非常喜欢 Z3。我觉得它被严重低估且使用不足，简直罪大恶极。几年前我曾用它做过一个相当有趣的用途：
https://www.oranlooney.com/post/playfair/#known-plaintext-at...
这比上面文档中展示的玩具示例稍微复杂一些，也暗示了 Z3 的一个真实世界用例——对密码学进行红队测试。
话虽如此，我不确定上面链接的文档在推广普及 Z3 方面是否真的帮了什么忙。
- greatgib
如果有人在问，因为我花了好几次跳转才找到答案：
Z3 是由微软研究院开发的一款高性能定理证明器。