Sözleşmelerin formal yöntemlerle oluşturulması, otomatik analiz edilebilirlik ve uygulayıcı akıllı kontratların otomatik olarak üretilmesi, izlenmesi gibi çeşitli faydalar sağlayabilir. Aşağıda alıntılanan, bu konudaki çalışmalardan sadece birisi.

Legal contracts specify the terms and conditions that apply to business transactions. Contracts are commonly expressed in natural language and contain many legal requirements that are often ambiguous, incomplete, and possibly inconsistent.

Smart contracts are programs intended to partially automate, monitor, and control the execution of legal contracts to ensure compliance with relevant terms and conditions.

Prof. Daniel Amyot at the School of Electrical Engineering and Computer Science of the University of Ottawa focuses on the formal specifications of legal contracts that can enable automated analysis and can support the generation of smart contract programs that monitor legal contracts. To that end, the Symboleo textual language was recently proposed, where contracts consist of collections of obligations and powers that define a legal contract’s compliant executions. Symboleo also offers execution time operations such as subcontracting, assignment, and substitution. The concepts underlying Symboleo are inspired from an existing legal ontology (UFO-L) with specialized contract concepts, with semantics described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations, powers, and other concepts. An encoding of Symboleo specifications in the nuXmv language, including a library of trusted modules capturing basic Symboleo concepts, enables the formal verification of properties of a contract, expressed in temporal logic (i.e., in LTL or CTL).  He has also experienced in two domains (food supply chain and transactive energy markets).