Smart Contract Verification
Tezos Japan, DaiLambda, Inc.
Jun FURUSE/古瀬 淳
FLOLAC’19, Taipei, 2019-08-29

Bit of myself: Past

OCaml researcher and programmer

  • Studied type system of FP
  • Like Haskell too

FP in Financial Systems

  • Derivative modeling
  • HFT(High Frequency Trading) systems

Bit of myself: Now

NPO to promote Tezos technology in Japan.

A small company to participate Tezos core development.

Bit of Tezos

  • 3rd gen. cryptocurrency
    (1st: Bitcoin, 2nd: Ethereum, 3rd: many)
  • Consensus algorithm: Proof of Stake
  • On Chain Governance
  • Symbol ꜩ

  • Written in OCaml
  • Formal verification

Today’s Agenda

  • Brief History of Currency
  • What is Blockchain?
  • Technical Aspects of Blockchain
  • Proof of Stake
  • Bit more about Tezos
  • Blockchain and Formal Verification

Brief History of Currency

Brief History of Currency

Main theme: “How to trade smoothly?”


👨 🌾 ⇄ 🐟 👩

Complex Bartering

👨 🌾 ← 🐟 👩
↘︎ ↗︎

Birth of Currency

👨 🌾 ⇄ 🐚 ⇄ 🐟 👩


China, 1100 BC

Monetaria moneta

Shell has a built-in value (beauty).

Conditions for Currencies

Scale of value (comparison of values)

Means of exchange (easy to carry)

Means of store of value (never rotten)


Mintable: Governments can control the money supply.

China, 800 BC (刀貨, 布貨)

  • Coins have built-in values as precious metal.
  • Seigniorage vs counterfait

Convertible Paper Money

Easier to carry

  • Assured conversion to gold (or silver, copper)
  • Total supply is limited to the government’s gold stock
  • The medium of the currency has no built-in value.
    → More strict anti-counterfait requirements

The First Convertible Paper Money

交子 in China, around 1050

  • Started as private notes for iron coins.
  • 宋 dynasty assured the conversion between copper coins.


This is not currency, but optimized trade efficiency
by recording credit/debt using numbers.

Fiat Money


Since 1971, at the end of Bretton Woods Agreements.

  • No more support by precious metal, but money stayed as money.
  • Confusions led to floating exchange rate system.
  • Governments can control their money supply.
  • Economy has boosted with more liquidity of currencies.

The First Fiat Money

交子 in China, around 1050, again.

  • The world first convertible paper money
  • … and soon became the world first fiat 😅
  • … and lost its value since too many were printed.

Electronic Money

No more medium. Just numbers in electrons.

  • Pegged with government currencies.
  • Very centralized. Manager companies are responsible for conversion.
  • Cryptography to prevent forgery and cheating.

The Basis of the Value of Currencies

Less and less:

  • The value of the medium: Nothing
  • Convertible with precious metal: No
  • The physical form as fiat: No

What Makes Money as Money?


  • Means of paying tax
  • You have to pay tax or you get arrested.

Radical Theory: Common Knowledge

Common knowledge that it is money.
With it, no need of centralized power!!

  • Iraqi Swiss dinar (1993-2003)
  • Somali shillings (1990’s)

Rise of Cryptocurrencies

Since 2009-01-03 (Bitcoin):

  • Electronic
  • Decentralized: no central bank
  • Cryptography to prevent counterfait and cheating

Tracking vs Privacy

Electronic money made tracking much easier.

  • Powers love tracking.
  • Public do not like being tracked.

Nowadays, anonymity is another important condition of currencies.