Securing People and their Machines Against Major Faults

1. 社交恢复的信息论基础——当私钥丧失时，无法再现原密钥，论文采纳社交信任替代：人选择新密钥，离链说服身份托管人超多数授权，朋友们在社交图中进行原子性的密钥替换。这避免了保存共享秘密的安全漏洞，将信任基础转向社交关系的可验证性。
2. 状态丧失的被动恢复设计——手机丢失但密钥保留时，每个代理维护"朋友的朋友"列表，周期性重广播检查点，丧失状态的代理被动吸收检查点直到完全恢复。该设计精妙地利用周期性消息克服了单次消息丢失，体现了对异步网络中信息论界限的深刻理解。
3. 三层形式化验证链——论文构造了从抽象规范到真实实现的完整验证链：(1)保护型多智能体原子交易定义状态转换和意愿守卫；(2)安全规范加入故障模型；(3)CVA中间抽象映射到异步消息传递。每层都有定理证明下层的实现正确性。这是形式方法的最佳实践，但要求每层假设的现实性验证。
4. 去中心化货币的超多数-交集最终性耦合——社交图允许"尽力"恢复（某些边可能无法恢复），但货币系统需要精确恢复以避免双花。论文采纳超多数写入和读取的交集结构：支付仅在超多数保管人持有时最终确定，恢复也从超多数收集。任何两个超多数相交保证了精确恢复和无意双花（定理7.3-7.4）。
5. 信息论不可恢复性的形式化处理——论文坦诚地界定了界限：当一条友谊仅被两个端点记录且至少一个端点丧失时，该边无法重构。论文通过可达性标志超时机制（Section C.15、C.33）确保丧失邻点最终从报告列表中被过滤，并明确排除此类边于"友谊保持"运行假设之外（Definition 4.8），这反映了对信息论边界的严谨认识。

本论文为形式方法论文，采用数学证明而非实证评估。规模指标：(1)形式证明50+个定理和引理，分布于主文和30+页附录；(2)覆盖四层完整验证链——抽象规范(Section 2)、安全规范(Section 4)、CVA中间抽象(Section 5)、应用到社交图和去中心化货币(Sections 6-7)；(3)关键验证包括：Theorem 4.11证明安全规范对原始社交图的F-弹性实现；Theorem 6.1-6.2证明CVA实现在静止状态下的正确性；Lemma C.6-C.33验证CVA层的11个不变量和6个活跃性性质；Theorem 7.3-7.4证明支付的精确恢复和无意双花防止。假设包括：(a)故障模型为仅崩溃故障（无拜占庭行为）；(b)最终同步网络（最终消息有界延迟）；(c)周期重广播机制（可靠交付）；(d)保管人可用性（超多数不永久失败）。