# Solidity 0.5: when typed does not mean type safe

## TL;DR

This paper critically examines Solidity 0.5's new type intended for safer Ether transfers, revealing that the compiler fails to enforce its guarantees, thus not improving type soundness over previous versions.

## Contribution

It identifies the shortcomings of Solidity 0.5's type system and proposes a formal methods-based solution to enhance type safety in smart contract programming.

## Key findings

- Solidity 0.5's new type is not effectively enforced by the compiler.
- Vulnerable patterns based on unsafe callbacks persist in Solidity 0.5.
- A formal methods approach can improve type safety and retroactively secure legacy code.

## Abstract

The recent release of Solidity 0.5 introduced a new type to prevent Ether transfers to smart contracts that are not supposed to receive money. Unfortunately, the compiler fails in enforcing the guarantees this type intended to convey, hence the type soundness of Solidity 0.5 is no better than that of Solidity 0.4. In this paper we discuss a paradigmatic example showing that vulnerable Solidity patterns based on potentially unsafe callback expressions are still unchecked. We also point out a solution that strongly relies on formal methods to support a type-safer smart contracts programming discipline, while being retro-compatible with legacy Solidity code.