Pacta sunt servanda: legal contracts in Stipula

TL;DR

This paper introduces Stipula, a domain-specific language designed to formalize and execute legal contracts, capturing core legal features and enabling implementation on centralized or distributed systems.

Contribution

It presents a formal semantics and a set of patterns for programming legal contracts, bridging legal content and executable code.

Findings

Stipula effectively models legal contract features like agreement and obligations.

The language's semantics enable precise understanding of contract behavior.

Examples demonstrate practical applicability to common legal templates.

Abstract

There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal content. We then undertake a foundational study of legal contracts and we distill four main features: agreement, permissions, violations and obligations. We therefore design Stipula, a domain specific language that assists lawyers in programming legal contracts through specific patterns. The language is based on a small set of abstractions that correspond to common patterns in legal contracts, and that are amenable to be executed either on centralized or on distributed systems. Stipula comes with a formal semantics and an observational equivalence, that provide for a clear account of the contracts' behaviour. The expressive power of the language is illustrated by a set of examples that correspond to template contracts that are often used in practice.