Formal Modeling and Analysis of Legal Contracts using ContractCheck

TL;DR

This paper introduces ContractCheck, a tool that formalizes and analyzes legal contracts, specifically SPAs, using logical encoding and SMT solvers to verify their consistency and executability.

Contribution

It presents a novel method for encoding legal contracts into first-order logic and automating consistency analysis with SMT solvers, enhancing legal contract verification.

Findings

Successfully encodes SPAs into structured logical assertions

Automates consistency checking using SMT solvers

Identifies contradictory clauses in legal contracts

Abstract

We describe a method and tool called \textit{ContractCheck} that allows for the consistency analysis of legal contracts, in particular Sales Purchase Agreements (SPAs). The analysis relies on an encoding of the premises for the execution of the clauses of an SPA as well as the proposed consistency constraints using decidable fragments of first-order logic. Textual SPAs are first encoded in a structured natural language format, called blocks. \textit{ContractCheck} interprets these blocks and constraints and translates them in first-oder logic assertions. It then invokes a Satisfiability Modulo Theories (SMT) solver in order to establish the executability of a considered contract by either providing a satisfying model, or by providing evidence of contradictory clauses that impede the execution of the contract. We illustrate the application of \textit{ContractCheck} and conclude by proposing directions for future research.