让重复报销不可表示：面向人类与 AI Agent 的已验证 Ethereum 电子发票系统

一篇 arXiv 论文提出基于 Ethereum 的完整电子发票系统设计、形式化分析与实现。作者将发票生命周期建模为带守卫的标签迁移系统，在标准密码学与共识假设下证明三项性质：报销唯一性（跨互不信任组织每张发票至多报销一次）、票面完整性、以及每个生命周期操作的授权可靠性。核心不变量用 Solidity SMTChecker 机器校验，并实现为 Solidity 0.8 合约与四角色 Web 应用。

现有中心化电子发票架构存在三个消费侧问题：发票可被重复提交报销、接收方难以验证真伪、数据集中形成性能瓶颈与单点故障。该工作把报销唯一性从“事后检测”变为“结构上不可表示”，并用机器校验的形式化证明支撑，而不是仅靠业务规则约束。

系统把每张发票建模为不可互换、不可转让的 NFT，状态经由五个带守卫子系统迁移，并采用基于锁的协议，使重复报销无法被构造出来。安全性依赖 keccak256 第二原像抗性等标准密码学假设与共识假设，核心不变量通过 Solidity SMTChecker 在所有可达交易序列上归纳验证，从而把跨组织信任问题交给链上状态约束。

对报销与发票类产品，这意味着防重复逻辑可从应用层的查重规则下沉到合约层的状态约束，跨机构场景下无需互信即可保证每票只报一次。私有 Ethereum 网络评测显示：开票约 646,773 gas，完整报销低于 135,000 gas，操作复杂度为 O(1)，可据此估算链上成本与吞吐设计。

• 在跨企业报销或对账场景做原型验证，复用 NFT 状态机与锁协议替代中心化查重服务。
• 针对 646,773 gas 开票与 135,000 gas 以下报销的成本结构，测算私有链或许可链的运营费用并与现有中心化方案对比。
• 把 SMTChecker 形式化验证流程引入自身合约研发，作为发票类状态机的不变量回归检查环节。
• 面向 AI Agent 消费侧，探索以链上发票状态作为可信输入，减少 Agent 对中心化验真接口的依赖。

• 论文摘要未说明吞吐与延迟指标，私有 Ethereum 网络在真实发票量级下的表现尚不明确。
• 授权可靠性的具体角色与密钥管理方案未在证据中展开，四角色 Web 应用的落地边界待确认。
• 未提供与现有中心化电子发票系统的合规或互操作方案说明。
• gas 成本随 Ethereum 主网价格波动的容忍度与补贴机制尚无证据支持。