This is an idea proposed in 2023 as a Cambridge Computer Science PhD topic, and has been completed by Derek Sorensen. It was supervised by Anil Madhavapeddy and Srinivasan Keshav as part of my Trusted Carbon Credits project.
Financial smart contracts routinely manage billions of US dollars worth of digital assets, making bugs in smart contracts extremely costly, and are also increasingly being used in other areas of endeavour such as carbon credit tracking. Because of this, much work has been done in formal verification of smart contracts to prove a contract correct with regards to its specification. However, financial smart contracts have complicated specifications, and it is not all straightforward for humans to write one which correctly captures all of its intended high-level behaviors.
To mitigate this challenge, this PhD explores the development of formal tools to target meta properties of smart contracts, which are properties of a contract that are intended by, but out of scope of, its specification. The targeted properties include the economic behaviors of the contract, properties relating to its upgradeability features, and the intended behaviors of systems of contracts. The formal tools presented are written in Coq.