我对形式化方法很感兴趣。我使用形式化方法来推理一些我一直在做的项目中的一些非常具体的子领域。我从未能够说服其他团队成员尝试相同的方法，更不用说使用形式化方法来指定整个领域了。
我发现特别有趣的一种方法是Alloy。我认为它可能更适合作为整个项目的基础，因为它在概念上和符号表达法上非常接近实际的编程语言。此外，工具相当可靠，因此模型验证的好处很容易获得。
如果你们在项目中使用Alloy的实际经验，我会非常感兴趣听听。你们觉得它帮助你们设计更好的领域模型吗？在验证过程中是否发现了领域模型中的错误？你们会再次使用它吗？
我曾在几个项目中使用过Alloy，并发现它非常有用。在其中一些项目中，我成功说服了其他人也使用Alloy或至少使用我编写的Alloy模型。这些项目可能不是您心目中所谓的“真实世界”项目，但它们确实发生在我工作的现实世界的某个部分。
2006年和2007年，我为当时的W3C XProc规范草案创建了部分Alloy模型；据我所知，大多数工作组成员从未阅读我写的论文（位于http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html），他们说：“哦，我们上周改变了规范的那部分，因此模型所述内容已经不再相关。”但这篇论文确实说服了规范编辑器，让他意识到第一版规范中描述的抽象“组件”级别存在严重问题，需要完全指定或去除。他去掉了它，对规范的可读性和可用性带来了好的效果。
2010年，我制作了一个XPath 1.0数据模型的Alloy模型，发现了规范中的一些缺陷。但是，大多数相关方（包括负责维护XPath 1.0规范的W3C工作组）的反应不太令人鼓舞。
我参与的一个研究项目使用Alloy对MLCD Overlap Corpus进行建模，这是我们正在创建的一组示例文档和相关信息（由于SO的要求，超链接被禁止）。Alloy模型在我们的语料库目录的初始设计中找到了一些错误，因此它非常值得投入精力。
我们还使用Alloy对转录性质以及将类型/标记区分扩展到文档结构的建模工作进行了一些形式化处理（可查看2010年Balisage会议的论文集）。这有点超出了Alloy通常应用的范畴，因为它与软件设计无关，但是Alloy检查模型的一致性和生成实例的能力在展示模型可能的公理逻辑后果方面非常有价值。
针对您的具体问题：是的，Alloy已经帮助我指定了更清晰的领域模型，并且发现了错误和故障。它们通常很小，原因是Daniel Jackson在他的书《软件抽象》中解释了这一点：首先，在设计过程中使用模型可以在一切仍然很小的时候就捕捉到错误。其次，正如Jackson所说：“事后看来，大多数软件设计问题都很琐碎。”
他继续说：“但是如果你不直接解决它们，琐碎的问题会变得非常重要。”我的经验充分证实了这一点。早期解决此类问题要好得多。所以是的，我会再次使用Alloy。
迟来的补充... 康银淑最近将 Alloy 应用于某些初创企业的 Web API 安全分析中（在安全领域中，Alloy 已被广泛应用，例如 Apurva 的 OAuth 分析 和 Barth 等人的 针对 CSRF 等浏览器安全机制的分析）; Pamela Zave 正在研究 Chord，一个点对点存储系统的令人印象深刻的分析，并最近撰写了对原始算法的修复。
是的，我曾经在工业上使用过Alloy及其类似工具。Alloy对我非常有帮助，它让我相信我的模型不是完全错误的，或者说它向我展示了哪些地方出现了错误，并导致了愚蠢的结果。其他更具体的工具，例如Song的Athena和Guttman以及Ramsdell的CPSA，在它们更狭窄的领域内更加有用。还有什么需要我告诉你的吗？
