# Set-Based Models for Cryptocurrency Software

## TL;DR

This paper discusses formal methods as a means to improve the security and correctness of smart contracts in cryptocurrencies, highlighting their potential to produce more reliable code.

## Contribution

It introduces formal methods techniques tailored for the cryptocurrency community to enhance smart contract security and correctness.

## Key findings

- Formal methods can produce bug-free, correct-by-construction smart contracts.
- Application of formal methods can bridge the gap between web code and nuclear-grade software.
- Partial application of formal methods improves software quality in blockchain applications.

## Abstract

Emin G\"un Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code [...] Yet the current Solidity language and underlying EVM seems designed more for the latter. Formal methods (FM) are mathematics-based software development methods aimed at producing "code for a nuclear power reactor". That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between "loose web code" and "code for a nuclear power reactor".