{"ID":2866604,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.20421","arxiv_id":"2509.20421","title":"Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)","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.","short_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 Mo...","url_abs":"https://arxiv.org/abs/2509.20421","url_pdf":"https://arxiv.org/pdf/2509.20421v2","authors":"[\"Reiner Hähnle\",\"Cosimo Laneve\",\"Adele Veschetti\"]","published":"2025-09-24T14:06:22Z","proceeding":"cs.SE","tasks":"[\"cs.SE\"]","methods":"[]","has_code":false}