Making Duplicate Reimbursement Unrepresentable: A Verified Ethereum E-Invoice System for Humans and AI Agents
A verified Ethereum e-invoice contract makes duplicate reimbursement impossible, including for LLM agents.
The paper designs an Ethereum e-invoice system that represents each invoice as a non-fungible, non-tradable token moving through five guarded subsystems. Under standard cryptographic and consensus assumptions it proves reimbursement uniqueness, keccak256 face integrity, and authorization soundness, with inductive invariants checked by Solidity SMTChecker. On a private network, issuance costs 646,773 gas, full reimbursement stays under 135,000 gas, and one node sustains 137 issuances per second. The verified contract is offered as a safety envelope that rejects duplicate, over-limit, or forged claims from LLM reimbursement agents.
- Proves an invoice is reimbursed at most once across organizations.
- Core invariants are machine-checked with Solidity SMTChecker.
- Issuance costs 646,773 gas; reimbursement stays under 135,000 gas.
- Contract rejects duplicate, over-limit, or forged LLM-agent claims.
Full article258 words · extracted from arxiv.org · click to collapse
Electronic invoices are replacing paper invoices worldwide, but today's centralized architectures leave three problems unsolved on the consumption side: an invoice can be submitted for reimbursement repeatedly, authenticity is difficult for recipients to verify, and data is siloed at a central authority that forms both a performance bottleneck and a single point of failure. This paper presents the design, formal analysis, and implementation of a complete blockchain-based electronic invoice system on Ethereum. We formalize the invoice lifecycle as a guarded labeled transition system and prove, under standard cryptographic and consensus assumptions, that the system guarantees: (i) reimbursement uniqueness--an invoice is reimbursed at most once, even across mutually distrusting organizations; (ii) face integrity--any verified invoice matches the recorded one unless keccak256 second-preimage resistance is broken; and (iii) authorization soundness for every lifecycle operation. The core invariants are machine-checked using Solidity SMTChecker, proving inductive validity across all reachable transaction sequences. The architecture models each invoice as a non-fungible, non-tradable token whose state transitions through five guarded subsystems, employing a lock-based protocol that makes duplicate reimbursement unrepresentable rather than merely detectable. We implement the design as a Solidity 0.8 contract with a four-role web application and evaluate it on a private Ethereum network: issuing costs 646,773 gas, full reimbursement costs under 135,000 gas, all operations run in O(1) time, and a single node sustains 137 issuances/s. Finally, the verified contract serves as a safety envelope for LLM-based reimbursement agents, provably rejecting unsafe actions (duplicate, over-limit, or forged-receipt claims) even when the agent's internal policy fails. All code and benchmarks are open-source.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.37819