Isabelle/HOL结合Z notation的HOL-Z、ZETA工具发布情况及替代方案咨询

• HOL-Z曾公开发布过，它是德国不来梅大学安全系统研究组的学术项目产出，专门用于实现Z notation到Isabelle/HOL的嵌入。但该项目在2010年前后就已经停止维护，仅支持Isabelle2005、Isabelle2009等老旧版本，早年的发布包目前没有公开的稳定留存渠道，因此现在无法检索到可用资源属于正常情况。
• ZETA是基于HOL-Z开发的扩展工具，主要新增了Z规范动画演示、测试用例自动生成的功能，该工具仅在项目参与团队内部使用，从未公开发布过正式版本，项目停摆后也没有相关资源公开流出。

• 借助Z/EVES工具配合转换脚本：Z/EVES是目前生态最成熟的Z notation开源分析工具，社区有第三方开源的转换脚本，可将Z/EVES格式的Z规范导出为Isabelle/HOL可识别的理论文件，仅需少量手动修正类型匹配问题即可使用，适合小型Z规范的验证需求。
• 复用已有Z语义嵌入实现：目前有多篇公开学术成果给出了Z notation的类型系统、操作语义在Isabelle/HOL中的完整嵌入代码，你可以直接复用这些代码在Isabelle环境中编写、验证Z规范，该方案适配最新版Isabelle，缺点是缺少原生Z语法糖支持，编写体验和专用Z工具存在一定差距。
• 经Event-B中间格式转换：你可以先将Z规范转换为Event-B形式，再通过Isabelle内置的Event-B导入插件将规范导入Isabelle环境进行验证，该路径的工具链成熟度较高，适配中大型Z规范的验证需求。

内容的提问来源于stack exchange，提问作者dordow