SymboleoNLP is a Web-based tool that allows contract authors to make customizations to a legal contract template using a controlled, yet expressive, natural language. The tool also maintains a formal specification of the contract in Symboleo, a formal specification language designed for the legal contract monitoring domain. The controlled customizations allow for the automated formalization of the customized contract, enabling Symboleo-based property verification and code generation of monitoring smart contracts. This work pushes the boundaries of requirements-based contract template customization with a view towards full formalization.

Automated formalization of legal texts in order to remove ambiguities, conflicts and incompleteness has been a challenge for Requirements Engineering (RE) research for decades. This work seeks to make an incremental step towards this objective for legal contracts by making use of contract templates. Our proposed approach starts with a natural language contract template, together with a manually formalized specification of that template. A contract writer can make customizations to the template, which trigger the automatic formalization of the corresponding customized contract. Our target specification language is Symboleo, which is created specifically for contract verification and monitoring. Starting with a manually formalized template reduces the complexity associated with a fully automated formalization. Typical contract templates use simple fill-in-the-blank parameters, which serve as customizations to formalize in our framing of the problem. Our approach pushes the boundaries of these templates by allowing the contract writer to enter complex natural language customizations, such as prepositional phrases and conditional statements. This work explores what types of natural language patterns can be used in that context by analyzing relevant linguistics and real legal contracts. It also introduces a tool, SymboleoNLP, that suggests the feasibility of the formalization process.