Deductive Verification of Legal Contracts

We enable deductive verification for Stipula, a domain-specific language for legal contracts, by systematically translating contracts into Java programs annotated with Java Modeling Language specifications, and subsequently proving them using a deductive verification tool. A central challenge of the translation lies in representing event-driven and time-dependent behaviour within a static specification framework. To address this, we introduce a dispatch table that records schedulable events together with their triggering times. The technique is presented for acyclic Stipula contracts. We also extend the proposed technique to cyclic contracts, outlining the additional challenges and the conditions under which the approach remains applicable.