Modeling and formally reasoning about distributed systems with faults is a challenging task. To address this problem, we propose the theory of Validating Labeled State transition and Message production systems (VLSMs). The theory of VLSMs provides a general approach to describing and verifying properties of distributed protocols whose executions are subject to faults, supporting a correct-by-construction system development methodology. The central focus of our investigation is equivocation, a mode of faulty behavior that we formally model, reason about, and then show how to detect from durable evidence that may be available locally to system components. Equivocating components exhibit behavior that is inconsistent with single-trace system executions, while also only interacting with other components by sending and receiving valid messages. Components of system are called validators for that system if their validity constraints validate that the messages they receive are producible by the system. Our main result shows that for systems of validators, the effect that Byzantine components can have on honest validators is precisely identical to the effect that equivocating components can have on non-equivocating validators. Therefore, for distributed systems of potentially faulty validators, replacing Byzantine components with equivocating components has no material analytical consequences, and forms the basis of a sound alternative foundation to Byzantine fault tolerance analysis. All of the results and examples in the paper have been formalised and checked in the Coq proof assistant.

翻译：对带有故障的分布式系统进行建模和形式化推理是一项具有挑战性的任务。为解决此问题，我们提出了验证标记状态转换与消息产生系统（VLSMs）的理论。VLSMs理论提供了一种通用方法，用于描述和验证其执行过程可能受故障影响的分布式协议的性质，并支持一种“正确性自构建”的系统开发方法论。我们研究的核心焦点是“含糊”（equivocation）——一种故障行为模式，我们对其进行了形式化建模、推理，并展示了如何基于系统中组件本地可获取的持久证据来检测它。含糊组件表现出与单迹系统执行不一致的行为，同时仅通过发送和接收有效消息与其他组件交互。如果系统组件的有效性约束能验证其收到的消息可由该系统产生，则该组件被称为该系统的“验证器”（validator）。我们的主要结果表明：对于由验证器构成的系统，拜占庭组件对诚实验证器造成的影响，与含糊组件对非含糊验证器造成的影响完全相同。因此，对于由潜在故障验证器构成的分布式系统，用含糊组件替代拜占庭组件不会带来实质性分析差异，并构成了拜占庭容错分析的另一种可靠基础。本文中的所有结果和示例均在Coq证明助手中进行了形式化验证与检查。