本文提出了一套面向密码学软件的全新形式化验证方法论，其核心取向是直接验证“生产级代码”，而不是为了便于验证而专门改写代码。作者选择 Rust 作为目标语言，看重的是它在性能与系统集成方面的优势：Rust 的所有权机制使 Aeneas 工具链能够把 Rust 代码抽取为 Lean 中的纯函数模型，从而免除对指针存活性、别名关系等底层细节的推理负担；Lean 的可扩展性又允许团队开发专用的策略（tactic）与库，大幅简化对抽取后代码的推理。工具链被专门设计并调优以配合 AI：智能体可以自主撰写形式化证明，这些证明由 Lean 内核独立校验；智能体还参与密码标准与平台相关 intrinsic 的形式化工作，但这部分仍需专家主导设计与评审。作者将该方法应用于微软的密码提供者 SymCrypt，验证了从其 C 版本移植到 Rust 的 SHA-3、ML-KEM 等算法实现；并进一步用实验性优化以及 FrodoKEM、ML-DSA、HPKE 等算法的实现来扩展 SymCrypt，以考察编写、移植与验证密码代码的可扩展性。整个 Lean 开发规模约 237 KLOC，为 16.7 KLOC 的 Rust 代码（覆盖 x86-64 与 ARM 平台上的后量子密码套件）建立了内存安全性、无 panic 以及功能正确性的证明。评估结果显示，经过验证的 Rust 实现能够满足 SymCrypt 在性能、可移植性、部署方式与可维护性方面的要求。

该论文提出「开放自动研究」(Open Autoresearch) 这一范式：人类与 AI 代理共同在一个公共排行榜上发布经评估器 (evaluator) 自动验证的改进成果，任何提升都必须可被机器复算检验。作者将其实例化为 ECDSA.Fail 基准，目标是优化可逆 secp256k1 椭圆曲线点加电路——这是 Shor 算法攻破椭圆曲线密码学的核心瓶颈。基准评分采用受时空类比启发的 S = Q × T，其中 Q 为峰值逻辑量子比特宽度，T 为平均实际执行的 Toffoli 门数，参赛者需最小化 S。结果显示，参与者将 S 降低了 86.1%。截至数据截断日(2026 年 7 月 26 日)，得分最佳的电路使用 1,151 个量子比特与 1,299,453 个平均执行 Toffoli 门，Q×T 约 14.96 亿；在不同记账约定下，比 Google 公开的点加分数阈值 (arXiv:2603.28846) 低 50% 以上。由于该基准将一个加数按经典方式提供，作者另外构建了一个与相干窗口化加法兼容的变体，实现窗口化 Shor 所需的单次调用接口：使用 1,162 个量子比特与 1,684,161 个平均执行 Toffoli 门；在 100,000 个随机输入上的经验成功概率为 0.99809，按可独立复跑的逐调用敏感度模型得到 Q×T/p̂ ≈ 19.61 亿，作者强调这不是完整 Shor 的成功率估计。其比特数与 Toffoli 数低于 Google 公布的阈值以及 Schrottenloher 报告的运行点 (arXiv:2606.02235)，但由于接口、记账约定与验证范围不同，不构成严格意义上的优越性证明。截断日后得分进一步降至 12.59 亿，另有低宽度电路降至 813 个量子比特。公开记录表明 AI 代理可与人类判断形成互补，为在可高效评估、可机器校验的目标上开展开放自动研究提供了证据。

持久化 AI 智能体通过反思、检索与整合构建自传式状态，但这种持久化仅改变信息的可用性，并未提升其认知地位——存储或检索到的内容并不能自动获得有效支持。因此，不受信任的输入、提示注入以及模型自身的推断都可能渗入持久状态，并在后续被系统误当作智能体的过往历史或用户的真实承诺。针对这一风险，论文提出一套类型化来源（typed provenance）与断言护栏（assertion guardrails）机制，用于实现“自传式断言有界性”（autobiographical assertion boundedness）——这是一种系统相对的释放性质，要求任何关于智能体、用户或指定关系的受控声明，都必须满足可接受证据、时间有效性与披露策略。其核心架构包括：类型化来源图，用于区分来源、依赖血统、认知角色、有效性与披露范围；解析器（resolver），负责评估授权状态投影，返回证据状态以及正交的冲突/过时/隐藏标志，并生成受保护的决策见证；生成-验证-修订（generate-verify-revise）中介，在候选语义单元被释放前对其进行一致性检查，并根据策略渲染状态响应。作者在显式假设（提取正确性、谓词正确性、解析健全性、视图去分类、信道中介等）下证明了一个条件性断言有界性契约。实验中，他们构建了24个手工编写的合规用例，相比flat/prior和source-tag比较规则（分别放行19/19和18/19个不安全候选），类型化中介在19个不安全机会中零个未被限定地通过，同时保留了全部5个受支持控制项。这些实验结论验证了解析器和中介的设计义务，但并不构成对语言模型或检索系统的端到端评估。

本文针对分布式系统与AI智能体中基于持有的授权模型（Proof-of-Possession）的局限性，提出了一种名为Proof-of-Continuity的权威传播时间模型。传统授权依赖令牌、凭证或能力等工件，但无法保证离散执行链中请求来源与后续步骤权威之间的因果关系，导致混乱代理（Confused Deputy）问题。本文提出的Provenance Identity Continuity（PIC）模型引入最小权威传播规则：每个执行步骤必须与前一步骤具有因果联系，且仅能传播来源授权上下文的一个非扩张子集。核心原语是Proof of Relationship（单跳因果原语），其传递闭包构成Proof-of-Continuity。该模型不是替代而是补充现有的证明持有模型。在此模型下，混乱代理条件无法成为有效模型行为——后续步骤的任何特权必须在来源授权上下文中已存在。该工作对分布系统与AI智能体特别相关，当执行器持有多个授权源调用工具和后端服务时，同一权威/因果错位问题跨服务边界反复出现。Proof-of-Continuity允许这些源一起携带但永不合并为组合权威，因为每个步骤仅针对导致其发生的血统授权上下文进行授权。论文侧重授权传播而非身份验证：OIDC、可验证凭证、钱包、工作负载身份等身份与认证机制仍是建立来源的补充手段，而Proof-of-Continuity解决来源存在后权威如何传播的问题。实验部分（摘要未提及）应在正文中展示模型形式化分析与安全性证明。适合分布式系统安全研究员、AI安全工程师、授权协议设计者阅读。