Reasoning for Smart contracts with Temporal Logic

Yoram Kornatzky
Oct 22, 2018 · 8 min read

We propose using temporal logic to reason on Ethereum smart contracts. These are initial first steps in our research intended to start a discussion in the blockchain community.

Smart Contracts

Reasoning on Smart Contracts

Temporal Logic of Concurrent Programs

Image for post
Image for post

Linear Temporal Logic

Branching Time Temporal Logic

Propositional vs First-Order Logic

Temporal Logic Operators

Liveness and Safety

The Blockchain as a Model of Time

Multiple Possible Timelines

Our Choice: Linear Temporal Logic

Is Time Discrete or Continuous?

Using Linear Temporal Logic for Describing Smart Contracts

A Basic Storage Smart Contract

contract BasicStorage {

uint storedData;

function set(uint x) {
storedData = x;
}


function get() constant returns (uint) {
return storedData;
}
}

Temporal Logic Statements for the Storage Contract

A Smart Contract for Real-Estate Purchase

contract Purchase {
address lawyer;
address buyer;
address seller;

uint256 amountDue;

uint256 startTime;
uint256 timeToLive;

bool approvedBuyer;
bool approvedLawyer;

constructor(address _buyer, address _seller, uint256 _amountDue, _uint256 timeToLive) public {
lawyer = msg.sender;
buyer = _buyer;
seller = _seller;
amountDue = _amountDue;
startTime = _timeToLive;
timeToLive = _timeToLive;
}

modifier canWithdraw() {
approvedBuyer && approvedLawyer;
_;
}

modifier didExpire() {
now > startTime + timeToLive;
_;
}

function approve() public {
if (msg.sender == buyer) {
approvedBuyer = true;
} else if (msg.sender == owner) {
approvedLawyer = true;
}
}

function() payable {
}

function withdraw(uint256 _amount) canWithdraw() public returns(bool) {
require(_amount < = this.balance);
require(msg.sender == seller);
require(msg.sender.transfer(this.balance));
}

function expire() public didExpire() returns(bool) {
require(msg.sender == buyer);
require(this.balance > 0);
require(msg.sender.transfer(this.balance));
}

}

Temporal Logic Statements for the Real-Estate Contract

Conclusions

Image for post
Image for post

2key

Re-Inventing the Link

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store