该论文针对电子发票在消费/报销侧长期存在的三个痛点——同一张发票可被重复提交报销、收票方难以验证真伪、数据集中托管在中心化机构从而形成性能瓶颈与单点故障——提出并完整实现了一套基于以太坊的电子发票系统。方法上，作者首先将发票生命周期形式化为一个带守卫（guarded）的标签迁移系统（labeled transition system），并在标准密码学假设与共识假设下证明了三条安全性质：(i) 报销唯一性，即一张发票至多被报销一次，即使参与方之间互不信任；(ii) 面额完整性，即任何通过验证的发票在 keccak256 抗第二原像性未被攻破的前提下与链上记录一致；(iii) 每个生命周期操作的授权健全性。核心不变量使用 Solidity SMTChecker 进行机器化验证，证明其在所有可达交易序列上归纳成立。架构上，每张发票被建模为一个不可互换、不可转让的 NFT 型代币，其状态在五个带守卫的子系统中迁移，并采用基于锁的协议，使“重复报销”在结构上不可表达（unrepresentable），而不仅仅是被检测出来。实现层面，作者用 Solidity 0.8 编写合约，并配套四角色的 Web 应用，在私有以太坊网络上进行评估：开票消耗 646,773 gas，完整报销低于 135,000 gas，所有操作均为 O(1) 时间复杂度，单节点吞吐可达 137 次开票/秒。此外，该经过验证的合约还被用作 LLM 报销智能体的安全外壳（safety envelope）：即使智能体内部的策略失效，合约也能可证明地拒绝不安全动作（重复、超额、伪造票据的报销请求）。所有代码与基准测试均已开源。该工作适合区块链安全、智能合约形式化验证、金融风控以及 LLM 智能体安全护栏方向的研究者与工程师阅读。