Formal Tools for Specifying Financial Smart Contracts
type: CreativeWork
description: Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. 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 to write one which correctly describes its intended behaviors. As a response to this challenge, we develop formal tools for specifying financial smart contracts. We target aspects of contract specification which are typically difficult to address and which can be a source of expensive contract vulnerabilities. In doing so, we hope to expand the capability of formal methods to specify desired contract behavior and thereby prevent catastrophic loss of funds.
abstract: Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. 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 to write one which correctly describes its intended behaviors. As a response to this challenge, we develop formal tools for specifying financial smart contracts. We target aspects of contract specification which are typically difficult to address and which can be a source of expensive contract vulnerabilities. In doing so, we hope to expand the capability of formal methods to specify desired contract behavior and thereby prevent catastrophic loss of funds.
author: Sorensen, Derek
language: eng
keywords: blockchain, formal methods, formal verification, interactive theorem prover, smart contract verification, smart contracts
license: https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/c43b7177-8daa-4859-b278-9fd28f30586e/download
license: http://purl.org/NET/rdflicense/allrightsreserved
date published: 2023-09-22
date modified: 2026-07-22T22:23:59Z
provider: Cambridge University
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: University of Cambridge

PropertyValue
property ID: DOI
value: 10.17863/CAM.118487