本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AIR）捕获Cairo语言的语义，该AIR断言存在满足特定代数约束的有限域值表。然后，加密交互式证明系统circle STARK提供一个高效验证的证书，证明AIR是可满足的。本文的核心贡献在于，利用Lean 4证明助手对AIR编码的可靠性（soundness）进行了形式化验证，即证明AIR的可满足性蕴含相应的计算性声明。这一验证确保了AIR编码不会错误地声称一个无效的程序运行完成。论文详细描述了验证过程，包括如何在Lean 4中形式化AIR的语义、约束以及soundness证明。该工作对于提高Cairo智能合约和区块链应用的安全性具有重要价值，因为它提供了一个数学上严谨的保证，防止因AIR编码错误导致的虚假计算声明。读者包括对形式化验证、区块链安全性以及零知识证明感兴趣的研究者和工程师。

本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[propext]（一个标准的mathlib4公理）限定，并集成在持续集成中。智能合约重入攻击自2016年以来已导致超过5亿美元的损失，其中DAO 2016攻击盗取了约360万ETH，并迫使以太坊硬分叉。OpenZeppelin ReentrancyGuard模式是生产DeFi中的事实标准防御措施，但此前没有工作建立其判别能力：即该防护能阻止对易受攻击实例的攻击，保持非攻击交易的正确执行，并区分相邻的安全和易受攻击变体。以往的工作要么形式化了玩具合约上的防护正确性，要么形式化了孤立实例上的攻击可行性，但未同时涵盖两个方向及针对生产源码的边界情况。本文通过变异测试验证了三种生产实例：DAO 2016、Compound v2和Aave V3的flashLoan，以及Aave V3 flashLoan的一个最小差异突变体（flashLoanVulnerable），该突变体隔离了一个安全关键差异。三方向结构包括：(a) DAO 2016模式的攻击复现，(b) Compound v2的正确性证明，(c) 区分Aave V3符合CEI模式的flashLoan与突变体的边界案例证明。一个顶层的元定理在“无改造”原则下组合了这三个方向，并在首次跨协议压力测试（从Compound v2到Aave V3）中进行了演示；更广泛的家族可移植性是未来工作。完整的Lean 4源码、CI配置和复现命令可在GitHub上获取。

本文针对密码系统侧信道攻击的掩码防御机制，提出了一种基于概率分离逻辑的形式化验证方法，用于自动验证掩码算法的非干扰性安全属性。作者首先建立了非干扰性与条件独立性之间的数学联系，从而将安全验证问题转化为条件独立性推理问题。随后，利用现有的Lilac分离逻辑框架（该框架专用于条件独立性推理）来执行验证，并设计了一系列新的证明规则，以支持探测安全性的高效验证。通过若干示例算法，论文展示了该方法能够有效验证典型掩码方案的安全性，同时相比传统手工证明或模型检验方法，降低了误判风险。该工作主要面向密码学实现者、安全验证工具开发者以及侧信道防御研究者，其核心贡献在于为掩码算法的形式化安全验证提供了更简洁、可自动化的理论框架。

该论文提出了Pramana，一个用于自治代理网络中的声明验证的协议层解决方案。在受监管领域中，自主代理对每个关键输出必须产生一个可审计的验证工件，记录声明内容、来源、执行者、时间和方式。当前的生产验证分为两个未标准化的方向：概率性判决模式（如自一致性投票、评审LLM集成）产生判断而非工件；而工件产生模式（如RAG、工具增强轨迹、生成器-验证器循环）产生特定于供应商的记录，外部审计员无法在不进行定制集成的情况下重构。Pramana定义了缺失的线路格式：每个关键代理输出被封装在一个类型化的ClaimAttestation中，包含四种变体（测量、推理、类比、引用），每种都配有针对记录源的verify()操作。对于测量声明和引用声明，verify()是确定性的；对于推理声明和类比声明，确定性则取决于预言机（在LLM支持下可审计重放）。这种四类分类源于古典印度认识论（pramana，有效知识的来源）。生命周期在TLA+中指定，并通过TLC在三个对称缩减模型上进行了全面验证：总共38,563个不同的可达状态，零个不变性违反。Python参考实现通过了84个测试。一个A2A和MCP的线扩展清单层叠了三个部署级不变性：可达性、SLA边界和离线可重新验证。一个探索性试点（n=100，2,275次评审调用）探讨了LLM作为代码生成中的评判者。最显著的观察是跨越语料库的40个百分点的原始FPR差异，与参考解决方案质量显著一致。该试点本身并不验证Pramana；结构论证和形式验证做到了这一点。

该论文提出一种混合SAT求解框架，将概率比特（p-bit）Ising采样器与经典冲突驱动子句学习（CDCL）求解器结合。传统CDCL求解器在可满足性实例上仍需大量冲突分析与布尔传播才能定位有效搜索区域。本文方法利用p-bit Ising采样器生成高一致性的文字（literals），作为临时假设传递给CDCL，旨在减少CDCL内部搜索开销。当采样假设导致矛盾时，CDCL回退到常规搜索。在受控骨干随机3-SAT基准测试上，混合方法相比纯CDCL减少中位冲突80.8-85.5%、中位传播80.2-84.6%。效益分布敏感，仅对特定实例类有效。进一步探索了机器学习门控机制，估计何时混合求解有益，随机森林门控保留94.8%的混合性能优势。该研究属于纯学术方法探索，无直接安全应用，但可能启发未来SAT求解效率提升。

该论文研究了在隐私敏感环境中，运行时监控系统如何保护敏感信息的问题。现代基于流的监控器会收集被观测系统运行时的详细统计数据，这些数据可能泄露隐私。差分隐私是保护敏感信息的先进方法，但将其集成到运行时监控中面临挑战：时序算子会导致单个输入值随时间影响多个输出，从而反复泄露隐私。论文提出了一种自动在基于流的监控规范中强制实施差分隐私的方法，通过分析时间依赖性并在规范中注入经过校准的噪声来实现。为了保持输出的效用，论文识别了规范中策略性的噪声注入位置，并利用基于树的机制来减轻聚合算子噪声注入带来的精度损失。通过在公共交通使用监控的案例研究，展示了该方法的实用性和有效性。