# Making Duplicate Reimbursement Unrepresentable: A Verified Ethereum E-Invoice System for Humans and AI Agents

arXiv: https://arxiv.org/abs/2609.37819 · HTML: https://mlsanity.com/paper/2609.37819/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 27 references that are in the map.
- First posted on arXiv 29 Sep 2026.

## Builds on (most cited first, 5 of 5)

- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Autonomous Agents on Blockchains: Standards, Execution Models, and Trust Boundaries](https://mlsanity.com/paper/2601.04583/) (2026)
- [An LLM Agentic Approach for Legal-Critical Software: A Case Study for Tax Prep Software](https://mlsanity.com/paper/2509.13471/) (2025)
- [A Blockchain-Based Approach for Secure and Transparent e-Faktur Issuance in Indonesia's VAT Reporting System](https://mlsanity.com/paper/2505.18157/) (2025)

## Abstract (arXiv)

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.