Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
Software Engineering
2025-09-29 v2
Abstract
Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications. As a verification backend, the deductive verification tool KeY is used. Both, the translation and the verification of partial and total correctness for a large subset of Stipula contracts, those with disjoint cycles, is fully automatic. Our work demonstrates that a general-purpose deductive verification tool can be used successfully in a translation approach.
Keywords
Cite
@article{arxiv.2509.20421,
title = {Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)},
author = {Reiner Hähnle and Cosimo Laneve and Adele Veschetti},
journal= {arXiv preprint arXiv:2509.20421},
year = {2025}
}