主要观点：

• 可使用 Porcupine 检查项目的严格一致性（线性化），如 etcd 和 TiDB 等实际系统所用，但其不能证明线性化，只能帮助建立信心。
• 通过示例展示如何用 Porcupine 检查分布式寄存器和分布式键值存储的线性化，包括定义模型、生成历史并验证等。

关键信息：

• 代码可在GitHub获取。
• 分布式寄存器类似单键的分布式键值存储，需定义输入输出及理想行为模型。
• 示例中给出了无效历史（并发设置后读取到不同值）和有效历史（无 stale read）的操作历史及可视化结果。
• 分布式键值存储的输入更复杂，模型状态和输出为map[string]int，历史也更复杂。

重要细节：

• porcupine.Model的Init函数初始化状态，Step函数处理输入、输出和状态转换。
• 用porcupine.CheckOperationsVerbose函数验证历史的线性化，若不满足则抛出异常。
• 提到 Porcupine 可通过分区状态空间提高性能等未涵盖的方面，以及后续可与“真实”系统连接等。