# Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)

arXiv: https://arxiv.org/abs/2509.20421 · HTML: https://mlsanity.com/paper/2509.20421/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Sep 2025.

## Built on by (most cited first, 1 of 1)

- [Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning](https://mlsanity.com/paper/2606.16118/) (2026)

## Abstract (arXiv)

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.