Detecting Legal Gaps in Standard-Form Consumer Contracts Through Formal Verification: A Model-Checking Approach Applied to Amazon France Terms of Sale
Antoine DAMON · Zenodo (CERN European Organization for Nuclear Research) · 2026
Standard-form consumer contracts contain implicit procedural structures states,transitions, guards, and invariants that constitutehidden nite state machines(FSMs).These implicit FSMs are never formally veried, leading to legal gaps, contradictions, andprocedural deadlocks that human readers systematically fail to detect. We present a frameworkthat (1) extracts FSMs from contract text using a dictionary of legal-to-formal patterns (J1J4), (2) formalises the extracted FSMs in Promela, and (3) veries legal properties via theSPIN model checker. Applying this framework to the Amazon France Terms of Sale (version1 August 2024, 9,608 words), we identifyseven formally proven legal gaps across threesub-FSMs (Order lifecycle, Right of withdrawal, Legal guarantee), exploring 858,790 states inunder three seconds. Six of the seven gaps involve the use of facultative modal verbs ( maydefer , may contact )where French consumer law imposes absolute obligations. One gap isstructural: the Force Majeure clause (Ÿ12) denes a blocking state with no exit path, creatinga formally proven deadlock. The seven gaps are individually cited with verbatim contract textand mapped to their violated legal provision. This work opens a research programme at theintersection of formal methods, contract law, and consumer protection, with applications toregulatory compliance auditing, LegalTech product development, and legislative drafting.