Introducing SmartPy and, an Intuitive and Effective Language and Development Platform for Tezos Smart Contracts


  • Use of the widely popular programming language Python, with its simple syntax and fast and elegant scripting possibilities.
  • Functional programming for clean and effective formal manipulations in OCaml as is already done in Michelson.
  • Static analysis and automatic proofs. The need for proofs is well understood in mission-critical industries and highly recognized in the Tezos community. A specific focus in the larger blockchain ecosystem is performed here with fully automatic proofs, especially through abstract interpretation.


  • A set of high-level primitives, SmartML, written in OCaml for a new smart contracts virtual machine that can be translated into Michelson. These primitives also exist on their own and can be executed, simulated and analyzed.
  • A Python library, SmartPy, providing a very intuitive and effective syntax that programmers can fully understand and use to directly access SmartML definitions. Today, Python is one of, if not the most, popular languages to do meta-programming in numerical analysis and machine learning with the multitude of Python frameworks: NumPy, TensorFlow, PyTorch, Scikit-learn, etc. SmartPy functions in a similar fashion: a programmer has access to the full power of Python and describes computational models with a regular Python library. These models are then evaluated elsewhere: on Tezos with SmartPy, in the cloud, on other CPUs or GPUs, etc. for numerical analysis or machine learning.
  • A compiler to translate SmartML contracts to Michelson.
  • Analytics — Analytics are elements of the user interface that provide some automatic procedures in to analyze and prove properties of smart contracts. They are not required to define smart contracts, but we believe that they are absolutely necessary for smart contracts to gain mainstream adoption by building trust among both developers and end-users.


Technical overview

Overview of from SmartPy to Michelson, Tests, and Analytics


An example

import smartpy as spclass StoreValue(sp.Contract):
def __init__(self, value):
self.init(storedValue = value)
def replace(self, params): = params.value
def double(self, params): = * 2
def divide(self, params):
sp.verify(params.divisor != 0) = / params.divisor

A few SmartPy constructions

  • Storage and parameters are readily available:
def messageName(self, params):
  • Some usual operators:
a = 3 * b + 2 # operations and affectations
a <= b # comparisons
  • Access to record fields, dictionary elements, arrays, etc.:
# Retrieving
# Setting
data.attribute = value


[sp.TRecord(groups = [sp.TRecord(contractWeight = sp.TInt,
ok = sp.TBool,
participants = [Rec(hasVoted = sp.TBool,
id = sp.address,
weight = sp.TInt)],
thresholdVoters = sp.TInt,
thresholdWeight = sp.TInt,
voters = sp.TInt,
weight = sp.TInt)],
groupsOK = sp.TInt,
name = sp.TString,
ok = sp.TBool,
thresholdGroupsOK = sp.TInt,
thresholdWeight = sp.TInt,
weight = sp.TInt)]
[...]                     # list/array
sp.TRecord(...) # record type
sp.TInt, sp.TBool, sp.TAddress, sp.TString # basic types
# for list
sp.list([v1, v2 , v3], t = ...)
# for any expression
sp.set_type(group.weight, sp.TInt)

Evaluation of SmartPy

An elementary example

    def remove(self, params):
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell <
sp.verify(1 <= k)
sp.verify(k <=[cell])[cell] =[cell] - k = 3 -

A little further with meta-programming

        if self.bound is not None:
sp.verify(k <= self.bound)

A complete example

import smartpy as spclass NimGame(sp.Contract):
def __init__(self, size, bound = None, winnerIsLast = False):
self.bound = bound
self.winnerIsLast = winnerIsLast
self.init(deck = sp.range(1, size + 1),
size = size,
nextPlayer = 1,
claimed = False,
winner = 0)
def remove(self, params):
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell <
sp.verify(1 <= k)
if self.bound is not None:
sp.verify(k <= self.bound)
sp.verify(k <=[cell])[cell] =[cell] - k = 3 -
def claim(self, params):
sp.verify(sp.sum( == 0) = True
if self.winnerIsLast: = 3 -
else: =


@addTest(name = "Test Store Value")
def test():
c1 = StoreValue(12)
html = c1.fullHtml()
html += c1.execMessage('replace', value = 15).html()
html += c1.execMessage('replace', value = 25).html()
html += c1.execMessage('double').html()
html += c1.execMessage('divide', divisor = 2).html()
html += c1.execMessage('divide', divisor = 0).html()
html += c1.execMessage('divide', divisor = 3).html()
@addTest(name = "Test Nim Game")
def test():
# Define of a contract
c1 = NimGame(size = 5, bound = 2)
# Show its representation
html = h2("Contract")
html += c1.fullHtml()
# Interact with the contract
html += h2("Message execution")
html += h3("A first move")
result = c1.execMessage("remove", cell = 2, k = 1)
# and update the html document we're creating
html += result.html()
html += h3("A second move")
result = c1.execMessage("remove", cell = 2, k = 2).html()
html += h3("An illegal move")
result = c1.execMessage("remove", cell = 2, k = 1).html()
html += h3("Another illegal move")
result = c1.execMessage("claim").html()
html += h3("A third move")
result = c1.execMessage("remove", cell = 1, k = 2).html()
html += h3("More moves")
html += c1.execMessage("remove", cell = 0, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 2).html()
html += c1.execMessage("remove", cell = 4, k = 1).html()
html += c1.execMessage("remove", cell = 4, k = 2).html()
html += h3("A failed attempt to claim")
html += c1.execMessage("claim").html()
html += h3("A last removal")
html += c1.execMessage("remove", cell = 4, k = 2).html()
html += h3("And a final claim")
html += c1.execMessage("claim").html()
c1.execMessage("remove", cell = 4, k = 1).html()
Executing: remove by [] at time [0].
cell = 0
k = 1
Result: OK
Claimed Deck NextPlayer Size Winner
False [0, 0, 0, 4, 5] 1 5 0

Taking this example further

  • Adding security verification to verify the identity of each player. This is typically done with some constructions like the following:
sp.verify( == sp.sender)
  • Defining a contract to play several Nim games in parallel where users can freely add new decks. Doing so helps reduce the cost of gas and allows for a more uniform landscape of smart contracts and dApps.
    This can be done by using a big_map for games.
def remove(self, params):
gameId = params.gameId
game =[gameId]
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell < game.size)
sp.verify(1 <= k)
sp.verify(k <= game.bound)
sp.verify(k <= game.deck[cell])
game.deck[cell] = game.deck[cell] - k
game.nextPlayer = 3 - game.nextPlayer
def claim(self, params):
gameId = params.gameId
game =[gameId]
sp.verify(sp.sum(game.deck) == 0)
game.claimed = True
sp.if game.lastWins:
game.winner = 3 - game.nextPlayer
game.winner = game.nextPlayer
with sp.if_(...):

Translating SmartPy to SmartML

(storage (record (claimed (bool False)) (deck (array "int" (int 1) (int 2) (int 3) (int 4) (int 5))) (nextPlayer (int 1)) (size (int 5)) (winner (int 0))) messages ((claim ((check (eq (sum (attrData "deck")) (int 0))) (set (attrData "claimed") (bool True)) (set (attrData "winner") (attrData "nextPlayer")))) (remove ((define "cell" (unknown 1)) (define "k" (unknown 2)) (check (ge (getParam cell (unknown 1)) (int 0))) (check (lt (getParam cell (unknown 1)) (attrData "size"))) (check (ge (getParam k (unknown 2)) (int 1))) (check (le (getParam k (unknown 2)) (int 2))) (check (le (getParam k (unknown 2)) (getItem (attrData "deck") (getParam cell (unknown 1))))) (set (getItem (attrData "deck") (getParam cell (unknown 1))) (sub (getItem (attrData "deck") (getParam cell (unknown 1))) (getParam k (unknown 2)))) (set (attrData "nextPlayer") (sub (int 3) (attrData "nextPlayer")))))))

Viewing SmartML

def claim(self, params):
sp.verify(sum( == 0) = True =
def remove(self, params):
cell = params.cell
k = params.k
sp.verify(cell >= 0)
sp.verify(cell <
sp.verify(k >= 1)
sp.verify(k <= 2)
sp.verify(k <=[cell])[cell] =[cell] - k = 3 -


  • Value domain analysis: which studies possible values taken by variables. This is the most important analysis and other analyses depend on it.
    Integers in Michelson use arbitrary precision so there is no overflow issues but this analysis still offers bound checking which is useful for gas and storage cost estimation and control.
  • Effects: determination of possible effects such as Payments.
  • Ownership: determination of who can change data in storage. A typical output of this analysis will be to determine a signature or a set of signatures that can change some storage. It would prevent bugs like the so-called MultiSig Parity Bug by construction and will be available for all smart contracts and not only the most important ones where an ad-hoc proof can be developed.
  • Workflow: graph of possible executions. This analysis is concerned with the sequencing of messages: ordering of messages, multiple calls, etc. It works by building a finite automaton approximation of the contract. Having the intended workflow for a contract helps prevent reentrancy or similar attacks.
  • Contract simplification: reduction of gas costs and complexity of contracts and storage.
  • Token conservation: verification of token attribution in a contract so that users know that their tokens cannot be misappropriated by others in contracts. The alternative could be to compute this property at runtime but it would cost gas and it would require a proof as well.
  • Time analysis. There are several notions of time in a blockchain. There is the real time used by every human activity with dates, hours, minutes, seconds, time zones, etc. And then there is “blockchain time” with the block time resulting from the sequence of blocks. Whatever time is used, it is important to check that a message to a contract can be made ‘on time’ and that a future event doesn’t happen either too early or too late in the future. This analysis studies contract execution timing.

Discussion about analytics vs ad-hoc proofs

  • Automatic analyses can be sound in the sense that they don’t claim something false but they cannot be complete in the sense that they cannot in general always answer the interesting questions they’re trying to answer.
  • Building an ad-hoc proof for a given contract in Coq is probably doable for every natural question we try to answer on every reasonable contract, but it’s probably quite costly and cannot be reasonably expected outside of a select small list of very important contracts.
  • Some analytics can present a result and may even be able to produce the ad-hoc proof in, e.g., Coq or part of it. We strongly think that this is a very nice research project.
  • These two approaches are non-exclusive in the sense that we can pragmatically start with an automatic analysis and see what it can or cannot do and continue from there to build an ad-hoc proof if deemed necessary.
  • The way analytics are designed in is really to focus on different dimensions (values, effects, ownership, workflow, etc.). Depending on the contracts, these questions will be useful or not. If a question appears repeatedly and is not answered by one of these analytics, it will probably be reasonable to add a new analysis to study it.

Next steps and tasks

  • Code base improvements
  • Editor improvements
  • Full determination of the list of constructions in SmartPy and implementation of all constructions of Michelson
  • Implementation and tests of the compiler to Michelson
  • Documentation and implementation of several example contracts
  • First public version of
  • Implementation of the analytics framework
  • Open source all software
  • Adaptation of the editor to possibly use a Javascript SmartJS library instead of the current Python SmartPy, the rest staying the same
  • Miscellaneous improvements of
  • Study and proof or verification of the compiler to Michelson
  • Optimization of compiler to Michelson possibly through Michelson to Michelson optimizations
  • Implementation of all the analytics
  • Use of SmartPy / SmartML to research potential improvements to Michelson




An intuitive and effective smart contracts language and development platform for Tezos. In Python.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

THM Advent-of-cyber 2021 Day21

Kubernetes practice environment setup on AWS EC2 with kubeadm

Understanding Python Decorators


NordVPN Status Indicator for GNOME

What happens when you type “ls -l *.c” in a linux command-line shell?

11 Tricks To Master the Art of Googling as a Software Developer

Drawing of Google search bar

How to Build a Chatbot from a Chatbot Template — A detailed guide — WotNot

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

An intuitive and effective smart contracts language and development platform for Tezos. In Python.

More from Medium

Day 91

Blockchain Technology and a New System for Political Elections:

Is Web 2 To Web 3 Bridge Possible?

Pecu Novus 2.0 : Code Falcon