Research Project: Lex Leibniz

Smart contracts on cryptocurrency platforms carry large amounts of monetary value, but have been prone to flaws and security vulnerabilities that have resulted in large financial losses.

This project is investigating the development of a high level smart contract language, suitable for the representation of financial contracts, that better supports the development of correct and secure smart contracts.

We are investigating the fundamental principles of smart contract verification, and developing ways of expressing financial contracts as smart contracts in ways that are more easily comprehensible to their users, and supports verification of both correctness and security.

The core methodological principle underlying the work is the use of declarative representations of smart contracts and their specifications. We will draw on earlier contributions to logic programming, deontic logic (the logic of permission, obligation and prohibition), work on logics for authentication and authorization in cryptographic settings and linear logic (as a representation of resource production, preservation and consumption).


Prof. Ron van der Meyden (CSE), Prof. Michael Maher (ADFA and Reasoning Research Institute),


Related earlier work: