Many aspects of everyday life are affected by legal documents, including wills and contracts. At the same time, the technological advances of recent decades have resulted in a steady migration of many aspects of life, both personal and professional, from the physical to the virtual. Because of this, activities governed by wills and contracts will increasingly be performed by software. To ensure the full access and trust of the public that will be relying on these systems, it is important to ensure that such software is accountable, meaning that the software should (1) verifiably follow all applicable rules and laws, (2) adapt appropriately to changes in laws, and (3) be explainable, so that non-programmers can understand what the code does and how it relates to what they intend. This project aims to develop a framework for the design and implementation of accountable software systems for wills implemented as smart contracts. The project will develop accountable software by combining expertise in the law with techniques from natural-language processing and formal methods for verifiable software generation and execution. The framework will include a two-stage translation process. In the first stage, natural-language legal documents (here, wills) will be translated into an intermediate semantic representation (Answer Set Programming) that can generate target smart-contract-language (Solidity) source code out of templated building blocks. In the second stage, the smart-contract language is then compiled into executable code that will be analyzed to ensure that the executable code faithfully represents the intended behavior. The translation will be explainable, meaning that each formal instruction can be traced back to the original human-understandable legal document text. The project will develop an annotated dataset that maps legal statements in natural language into the intermediate representation and use this to adapt deep-learning techniques that have revolutionized the machine translation of natural languages from wills to code. The framework will guarantee that the translation and execution of a will is faithful to the will and the law using two complementary methods: (1) It will check the translated formal representation against laws written in natural language using a natural-language inference module that is able to assess whether the original text expressed in the will in the context of creation and execution is consistent with relevant legal text, and (2) the executable code will be analyzed using compiler technology to reason about the semantic similarity between the validated source code of the contract and its decompiled executable. The project will have significant positive impacts on society, in terms of both computing technology and law: it will develop novel techniques and tools to translate human-understandable contracts to machine-understandable smart contracts in a well-defined and explainable way, and it will validate the resulting executable code against the original contracts. During the project, the researchers will also identify legal regimes that can be successfully automated and improve accountability. All of the software and data produced during this research will be made freely available to the research community. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.