StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification
该论文处理的是一个在可验证计算工程中常被忽视的信任缺口：GKR 协议的可靠性界只能保证『关于某个算术电路的输出声明是可信的』，却无法保证『该电路确实编码了应用所期望的状态转移』。作者以稀疏 Merkle 树（SMT）的成员证明、非成员证明与
#formal-verification
共收录 95 条相关情报。
← 返回所有主题Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation
该论文关注神经网络“机制编辑”的可验证性，即通过消融、权重编辑或激活引导，从模型中移除某一有害能力（或技能），同时尽量保留其他有用能力。现有做法通常只靠测试集验证编辑效果，但有限测试无法覆盖连续、无穷的输入空间，因此无法保证在所有输入区域都
A Fourier-Label Information-Loss Barrier for Dihedral Coset Algorithms
本文针对二面体陪集问题（DCP, Dihedral Coset Problem）建立了一条“不可行性”（no-go）定理，属于量子算法与后量子密码学的交叉理论研究。DCP 是 Regev 于 2004 年提出并用于将格上学习带误差问题（LW
Making Duplicate Reimbursement Unrepresentable: A Verified Ethereum E-Invoice System for Humans and AI Agents
该论文针对电子发票在消费/报销侧长期存在的三个痛点——同一张发票可被重复提交报销、收票方难以验证真伪、数据集中托管在中心化机构从而形成性能瓶颈与单点故障——提出并完整实现了一套基于以太坊的电子发票系统。方法上，作者首先将发票生命周期形式化为
Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
该论文研究如何让大语言模型（LLM）可靠地参与安全协议的形式化建模。背景是：安全协议（如认证与密钥交换协议）的安全性通常需要借助 Tamarin 这类形式化验证工具来证明，而把自然语言写的协议描述（RFC、规范文档）翻译成可验证的形式化模型
LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?
本文针对一个此前缺乏系统认识的问题展开研究：大语言模型（LLM）在密码协议的符号化验证（symbolic protocol verification）中究竟能起到多大作用。作者指出，LLM 已在软件工程与安全分析任务中表现出较强潜力，但其在
RAISE: Reinforcing Access Control Policy Synthesis in LLMs via Symbolic Evaluation
该论文关注一个在云权限治理中极具现实意义的问题：如何把自然语言描述的访问控制需求，可靠地翻译成形式化、可验证的授权策略。作者指出，这类转换并不只是语法层面的翻译，而需要对权限、约束与例外条件进行严格推理，即便当前最前沿的大模型也常常生成语义
Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation
当前主流神经网络推理依赖存放在高带宽显存中的稠密浮点权重矩阵，既受严重的内存墙瓶颈制约，也无法在以太坊虚拟机（EVM）等确定性虚拟机上原生执行。而在 Blum-Shub-Smale 模型下，对连续域上递归动力系统的终止性与算术不变量做验证一
SADRA: Sound Capability-based Access Control System for Resource-Disaggregated Architectures
该论文研究的是资源解聚（resource disaggregation）架构下的访问控制问题。在这种架构中，内存、加速器等资源被从计算节点上物理分离，并通过网络被远程访问，从而提升资源利用率与共享效率；但代价是本地内核被移出资源访问路径，资
Steelhead: Interleaving Partially Synchronous and Asynchronous Commit Rules on a Shared DAG
该论文提出 Steelhead——一种双模式共识机制，目标是兼得部分同步协议的高性能与异步协议在恶劣网络条件下的存活性。现有 DAG 类 BFT 协议通常二者只能取其一：部分同步提交规则在健康网络中快，但一旦网络状况超出同步假设就会停滞；异
Automated Abstraction Refinement for Information Flow Security in Embedded Systems
本文聚焦安全敏感嵌入式系统的信息流安全验证问题。信息流分析（IFA）是验证机密性与完整性的重要手段，但嵌入式系统天然具有并发性与时间相关性，导致既有 IFA 方法往往陷入两难：要么抽象过于粗糙而精度不足、无法判定非法信息流是否存在，要么保持
Formally Modeling the Terrapin Attack on SSH
该论文针对 SSH 通道完整性，提出一个在“部分选定状态”（partially chosen state）下形式化建模的框架，以回答 Terrapin 攻击（USENIX Security 2024）留下的开放问题：在 Terrapin 攻
Staged Multi-step UTXO Workflows via Recursive Invariants
该论文针对无状态 UTXO（未花费交易输出）风格的账本执行模型提出了一套名为「递归不变量」（Recursive Invariants, RI）的交易级逻辑与工具链，用以支撑多步工作流。背景问题是：UTXO 模型只依据本地数据和被引用数据即可
Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults
本文提出 Hydrozoan，一个面向混合故障模型的 DAG（有向无环图）共识协议。背景是：基于 DAG 的共识可达很高吞吐，并在 n=3f+1 的经典设定下达到最优的三消息延迟下界；已有的两消息延迟协议要么靠牺牲容错度（例如需要 5f+1
SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
该论文聚焦于硬件形式化信息流验证（Information-Flow Verification, IFV）在真实 RTL 上难以扩展的问题。IFV 能为「无秘密依赖的时序与控制行为」提供强保证，但在实际设计中，证明往往因求解器规模爆炸而超时。
MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs
背景与问题：LLM 编码智能体（coding agent）如今能够以远超人工审查速度的规模生成复杂程序，这带来了显著的安全与可靠性风险。常见检测手段——模糊测试、静态分析、LLM-as-a-Verifier——虽然能发现大量缺陷，但难以覆盖
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
该论文关注形式化验证与软件保障中的基础原语——UNSAT 证明（不可满足性证明）。在实际工程中，SAT/SMT 求解器生成的证明往往编码了专有逻辑、内部约束或安全敏感信息，直接公开披露会导致知识产权泄露或攻击面暴露。零知识 UNSAT 认证
CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness
LLM 智能体（agent）会生成并执行多步计划，计划中会调用外部工具；这些工具既可访问私有数据，也可执行命令。在此场景下，安全性并非某个单一步骤的属性，而是由计划所形成的整个执行过程的属性；计划本身就是关键工件，记录了工具调用、控制流与数
SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
基于能力（capability）的架构如 CHERI 为软件组件的架构级隔离提供了强支持：能力指针同时携带边界与权限，使硬件能够阻止越权访问。然而攻击者还可利用微架构侧信道窃取机密，因此敏感代码通常需以常量时间（constant-time）
Understanding the Usability of Cryptographic Verification Tools
该论文针对密码学协议形式化验证工具的实际使用体验开展了一项以人为中心的探索性研究。作者指出，Tamarin、ProVerif 等协议验证工具已被广泛用于分析复杂协议的安全性，但用户如何与这些工具交互、在哪里受阻，长期以来缺乏系统性研究。为此