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

Jia Cai

cs.CRSep 29, 2026

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

Authors: Jia Cai

Organizations: College of Engineering and Computing George Mason UNiversity Fairfax, VA, USA

Abstract

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.

Figures & tables

System	Platform	Invoice model	Lifecycle coverage	Digest verification	Red-flush	Duplicate-reimburse prevention	Formal proofs / open source
Zhang & Liu ’17 [ 12 ]	Conceptual	data record	issuance (sketch)	▲	✗	✗	✗ / ✗
Hyvärinen et al. ’17 [ 10 ]	Ethereum	refund claim	dividend-tax refund	▲	✗	✓ (refund)	✗ / ✗
Shenzhen/Tencent ’18 [ 13 ]	Consortium	data record	issue $\to$ reimburse	✓	▲	▲ (closed)	✗ / ✗
Fatz et al. ’19 [ 11 ]	Ethereum	process instance	VAT process validation	▲	✗	✗	✗ / ✗
Nguyen et al. ’19 [ 15 ]	Ethereum + DSN	data record	issue + VAT payment	✓	✗	✗	✗ / ✗
Farchan ’24 [ 16 ]	Hyperledger Fabric	data record	issue + reporting	✓	✗	✗	✗ / ✗

TABLE I: Comparison with representative blockchain e-invoice / tax systems. ✓ = supported, ▲ = partial or proprietary, ✗ = not addressed.

Symbol	Meaning
$\mathcal{A}$	address space; $b\in\mathcal{A}$ the tax bureau
$\mathcal{N}$	invoice-number space (nonzero)
$R\subseteq\mathcal{A}$	registered enterprise accounts
$O:\mathcal{N}\rightharpoonup\mathcal{A}$	invoice owner (undefined $=$ nonexistent)
$\mathsf{st}:\mathcal{N}\to Q$	lifecycle status, $Q$ from Def. 3
$\mathsf{cr}:\mathcal{N}\to\{0,1\}$	credit-note flag

TABLE II: Notation for the formal model.

Operation	Guard (precondition)	Effect (state update)
$\mathsf{register}(c,a,\mathit{id})$	$c=b\,\wedge\,a\notin R$	$R\mathrel{+}=a$
$\mathsf{mint}(c,n,a)$	$c=b\,\wedge\,a\in R\,\wedge\,O(n){=}\bot$	$O(n){:=}a;\ \mathsf{st}(n){:=}\textsc{Blank}$
$\mathsf{issue}(c,n,v,\phi)$	$c\in R\wedge O(n){=}c\wedge\mathsf{st}(n){=}\textsc{Blank}\wedge v\in R\wedge v\neq c\wedge\mathit{valid}(\phi)$	$F(n){:=}\phi;\ \mathsf{st}(n){:=}\textsc{Issued};\ O(n){:=}v;\ D(H(\phi)){:=}n$
$\mathsf{redFlush}(c,n,m)$	$c\in R\wedge\mathsf{st}(n){=}\textsc{Issued}\wedge\mathsf{cr}(n){=}0\wedge\mathsf{sel}(n){=}c\wedge O(m){=}c\wedge\mathsf{st}(m){=}\textsc{Blank}$	$F(m){:=}F(n),\ \mathsf{cr}(m){:=}1;\ \mathsf{st}(n){:=}\textsc{Reversed};$ $\mathsf{st}(m){:=}\textsc{Issued};\ O(m){:=}\mathsf{buy}(n);\ D(H(F(m))){:=}m$
$\mathsf{declare}(c,n)$	$c=\mathsf{sel}(n)\wedge\mathsf{st}(n)\notin\{\textsc{None},\textsc{Blank}\}\wedge\mathsf{cr}(n){=}0\wedge\mathsf{dc}(n){=}0$	$\mathsf{dc}(n){:=}1$
$\mathsf{lock}(c,n,\mathit{cid})$	$\mathsf{st}(n){=}\textsc{Issued}\wedge\mathsf{cr}(n){=}0\wedge O(n){=}c\ [\wedge\ \mathsf{dc}(n){=}1]$	$\mathsf{st}(n){:=}\textsc{Locked};\ L(n){:=}(c,\mathit{cid})$

TABLE III: Guarded transition rules (per invoice

n

c

is the caller. All guards are conjunctive; a failed guard reverts with no effect.

Operation	Gas (mean)	Time	Storage
registerEnterprise	189,326	$O(1)$	$O(1)$
applyForInvoices	92,918	$O(1)$	$O(1)$
grantInvoices (per blank)	140,731	$O(k)$	$O(k)$
issueInvoice	646,773	$O(1)$	$O(1)$
redFlush	696,130	$O(1)$	$O(1)$
declareTax	32,716	$O(1)$	$O(1)$

TABLE IV: Per-operation gas cost and complexity (

N

invoices, batch size

k

Claim	Nature	Decided by	Outcome
C1–C3	legitimate	contract	reimbursed on-chain
C4	duplicate of C1	policy	rejected: “Reimbursed, not Issued”
C5	over spending limit	policy	rejected: exceeds ¥5,000 ceiling
C6	forged receipt (amounts $\times 2$ )	policy	rejected: digest verification fails
C4 ′	duplicate, policy bypassed	contract	reverted: “not available for reimbursement”
Unsafe actions executed on-chain: 0 of 4 attempts. Audit: 6 invoices, 0 findings.

TABLE V: Reimbursement-agent case study (deterministic reasoner; six claims over five seeded invoices; local chain).

Explore similar work

Sep 2, 2026cs.AI

ClaimReceipt: Verifying Evidence Sufficiency and Coverage in Agent Evaluations

Agent evaluations face two distinct evidentiary questions: whether a reported claim is recomputable from retained evidence (sufficiency), and whether the retained records cover the committed experiment set (coverage). Generic logs and hash-linked transcripts answer neither reliably. We introduce ClaimReceipt, a claim-relative receipt specification and selective verifier that binds typed transaction evidence to a signed experiment manifest and returns PASS, INVALID, or INCONCLUSIVE per claim. We freeze the specification before implementation (SHA-256 18d109...b81). On 1,392 historical buyer--seller records, a CR-2 verifier reproduces all five manually labeled audit verdicts, exactly replays 600 deterministic and 792 post-generation records, makes every one of 13 declared field groups non-redundant under tested ablations, and returns the expected result on 11/11 semantic faults with 0/8 false positives. We then run a separate prospective CR-3 epoch: 30 assignments are committed before inference, terminal receipts are signed and chained, and private evidence is encrypted for an auditor. Complete evidence yields coverage and accounting PASS; withholding one terminal receipt returns INCONCLUSIVE_COVERAGE, while withholding all private openings preserves coverage and protocol verification but makes economic claims inconclusive, exactly matching a preregistered prediction. Receipt instrumentation adds 0.021% of model-inference time and 9.9 KB per transaction. A specification-legibility probe indicates that our own frozen specification is not yet unambiguous to an independent reader. Claim verification therefore requires both claim-sufficient evidence and a committed universe against which omissions become visible.

Peiying Zhu, Sidi Chang

Blossom AI Blossom AI Labs San Francisco, CA, USA

Category-Aware Atomic Claims Transaction Evidence

Ask PDF

Apr 23, 2026cs.CR

Who Audits the Auditor? Tamper-Proof Fraud Detection with Blockchain-Anchored Explainable ML

In enterprise fraud detection, model accuracy alone is insufficient when insiders can tamper with audit logs or bypass approval workflows. Real-world incidents show that fraud often persists not because detection algorithms fail, but because the audit trail itself is controllable by privileged operators. This exposes a fundamental trust gap: who audits the auditor? We present a tamper-evident fraud detection system that anchors both ML predictions and workflow execution to an immutable blockchain ledger. Rather than using blockchain as passive storage, we enforce the entire approval process through smart contracts, ensuring that every transaction, prediction, and explanation is atomically recorded and cannot be retroactively modified. Our detection module achieves competitive accuracy (F1 = 0.895, PR-AUC = 0.974) while providing cryptographically verifiable decision trails that support regulatory auditability requirements (e.g., GDPR Article 22). System evaluation shows sub-25 ms inference latency and economically viable deployment on Layer-2 networks at under $0.01 per transaction (validated against PolygonScan data), supporting enterprise-scale workloads of 10,000+ monthly payments.

Zhaohui Wang

Viterbi School of Engineering University of Southern California Los Angeles, CA, USA

Fraud Detection Model Auditing Blockchain Tamper Localization Ledger

Ask PDF

Dec 7, 2025cs.CE

TxSum: User-Centered Ethereum Transaction Understanding with Micro-Level Semantic Grounding

Understanding the economic intent of Ethereum transactions is critical for user safety, yet current tools expose only raw on-chain data or surface-level intent, leading to widespread ``blind signing'' (approving transactions without understanding them). Through interviews with 16 Web3 users, we find that effective explanations should be structured, risk-aware, and grounded at the token-flow level. Motivated by these findings, we formulate TxSum, a new domain-grounded NLP task for DeFi transaction explanation, and construct a dataset of 187 complex Ethereum transactions with 2,375 token-flow annotations and transaction-level summaries. We further introduce MATEX, a grounded multi-agent framework for high-stakes transaction explanation. It selectively retrieves external knowledge under uncertainty and audits explanations against raw traces to improve token-flow-level factual consistency. MATEX achieves the strongest overall explanation quality, especially on micro-level factuality and intent quality. It improves user comprehension on complex transactions from 52.9% to 76.5% over the strongest baseline and raises malicious-transaction rejection from 36.0% to 88.0%, while maintaining a low false-rejection rate on benign transactions.

Zifan Peng, Jingyi Zheng, Yule Liu +8

1Hong Kong University of Science and Technology (Guangzhou) · 3Independent Researcher · University of North Texas +2

Bitcoin Transaction Evidence Explainable AI Methods Summarization High-Stakes Domains

Ask PDF