The formalization of natural language contracts can make the prescriptions found in these contracts more precise, promoting the development of smart contracts, which are digitized forms of the documents where the monitoring and execution can be partially automated. Full formalization remains a difficult problem, and this thesis makes steps towards solving this challenge by focusing on a narrow sub-problem of formalizing contract refinements. We want to allow a contract author to customize a contract template, and automatically convert the resulting contract to a formal specification language called Symboleo, created specifically for the legal contract domain. The hope is that research towards partial formalization can be useful on its own, as well as useful towards the full formalization of contracts. The main questions addressed by this thesis involve asking what linguistic forms these refinements will take. Answering these questions involves both linguistic analysis and empirical analysis on a set of real contracts to construct a controlled natural language (CNL). This language is expressive and natural enough to be adopted by contract authors, and it is precise enough that it can reliably be converted into the proper formal specification. We also design a tool, SymboleoNLP, that demonstrates this functionality on realistic contracts. This involves ensuring that the contract author can input contract refinements that adhere to our CNL, and that the refinements are properly formalized with Symboleo. In addition to contributing an evidence-based CNL for contract refinements, this thesis also outlines a very clear methodology for constructing this CNL, which may need to go through iterations as requirements change and as the Symboleo language evolves. The SymboleoNLP tool is another contribution, and is designed for iterative improvement. We explore a number of potential areas where further NLP techniques may be integrated to improve performance, and the tool is designed for easy integration of these modules to adapt to emerging technologies and changing requirements.

Smart contracts are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are among the most popular choices for smart contract development. However, there is a substantial gap in the knowledge of smart contracts between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. This thesis proposes a tool-supported method for translating Symboleo specifications into smart contracts. Its contributions include extensions to the existing Symboleo IDE, the implementation of the ontology and semantics of Symboleo into a reusable library, and the Symboleo2SC tool that generates Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. Experimentation with Symboleo2SC shows that legal contract specifications in Symboleo can be fully converted to smart contracts for monitoring purposes. Moreover, Symboleo2SC helps simplify the smart contract development process, saves development effort, and helps reduce risks of coding errors.