Towards the Specification and Verification of Legal Contracts

A contract is a legally binding agreement that expresses high-level requirements of parties in terms of obligations, powers and constraints. Parties' actions influence the status of a contract and shall comply with its clauses. Manual contract monitoring is very laborious in real markets, such as transactive energy, where plenty of complex contracts are running concurrently. Furthermore, liability, right and performance transition through run-time operations such as subcontracting, assignment and substitution complicate contract interpretation. Automation is needed to ensure that contracts respect desirable properties and to support monitoring of compliance and handling of violations. In this thesis research, I propose an innovative ontology that defines fundamental contractual notions (such as the ones mentioned above) and their relationships, on which is built a specification language, called Symboleo, that provides syntax and axiomatic semantics of contracts via first-order logic. Symboleo enables the development of advanced automation tools such as a compliance checker that monitors contracts at runtime, and a model checking verification method that analyzes liveness and safety properties of contracts. This paper reports on the problem domain, research method, current status, expected contributions, and main foreseen challenges.