Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912607653330944 |
|---|---|
| author | Hähnle, Reiner Laneve, Cosimo Veschetti, Adele |
| author_facet | Hähnle, Reiner Laneve, Cosimo Veschetti, Adele |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_20421 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version) Hähnle, Reiner Laneve, Cosimo Veschetti, Adele Software Engineering 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. |
| title | Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version) |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2509.20421 |