为 AI 智能体立宪:Charter 用 Lean4 打造形式化验证的规则语言

QuixiAI · x · 2026-11-06

QuixiAI 宣布其 Sovereign Protocol Language(SPL)演进为 Charter——一个基于 Lean 4 构建、并通过 eFLINT 全部测试的超集 DSL。

Charter 定位为「形式化验证的机构语言」,用于表达宪法、协议、章程、合同与规章等制度规则。它最初是为了形式化主权智能体协议(Protocol of Sovereign Agency, PSA)而造——一套约束自主智能体权利、义务、责任、谱系与自我修正的「新机器人法则」框架,但设计上不含任何协议特定原语,全部构造(事实、行为、义务、权力、豁免、时间、模块、出处溯源)都是通用制度结构。作者此前评估 Veil、Catala、L4、Quint 均表达力不足,遂自建此语言。项目已开源。