SMT-Based Automated Verification for Financial Transaction Document Consistency

Abstract

This work report our intial result on automated verification for MT940 (a standardized electronic bank statement message used on the SWIFT network) using SMT Z3 solver. Since there is no consistency check of the financial values inside the transaction data that is sent to external parties in structured report formats of MT940, an integrated automated validation pipeline is must existing need. In this work, The pipeline is placed after CSV generation and before MT940 conversion. It operates in three sequential stages that are format and structure validation, metadata extraction, and formal SMT verification. Financial rules are encoded as logical constraints and checked simultaneously, producing a SAT (consistent) or UNSAT (inconsistent) verdict. Because the verification step operates on six aggregate metadata parameters rather than individual transaction rows, solver complexity is constant with respect to data volume. The pipeline complexity remains linear in the number of transactions due to the metadata extraction stage. Our result shows a promising automated model for banking document transaction checking.