FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens

Nomadic Labs is looking for a FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens intern. Tutors: Arvid Jakobsson, Kristina Sojakova Blockchains, such as Tezos, implement t

Nomadic Labs is looking for a FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens intern.

Tutors: Arvid Jakobsson, Kristina Sojakova

Blockchains, such as Tezos, implement tokens: cryptographically secured assets representing the ownership of a value. Chains typically have one native token (in the case of Tezos; the tez), but also allow developers to create additional tokens for other types of value. In Tezos, this is done by writing a smart contract: a small piece of software deployed on-chain. The smart contract defines how tokens are created, removed and transferred between users.
Interoperability of token contracts is important: they form key components in larger systems of inter-acting smart contracts. The FA1.2 standard have been proposed as a common interface all token contracts should expose. In addition, security of token contracts is clearly paramount: we wouldn’t want any tokens to get lost or stolen. For these reasons, Nomadic Labs have formalized the FA1.2 standard using Mi-Cho-Coq, a smart-contract verification platform for Tezos. Using it, we have ensured standard compliance of several popular FA1.2 implementations, and increased our confidence in their security.

Goals

Currently, a correctness proof must be hand-written to verify compliance with the formalized standard. This is time consuming and requires Coq expertise beyond the average smart contract developer. The first step of this internship is to use the FA1.2 formalization as base for implementing a compliance testing suite in Coq. The intern should prove in Coq, using the standard’s formalization, that each compliant token contract must pass the verification of the test suite. In other words: prove that the compliance suite itself is coherent with respect to the standard.
In the second step, the intern will make the conformity-testing tool available through an online interface. Smart contract developers will be able to test the compliance of their smart contract from the comfort of their browser, without having to install Coq or write any proofs.

Requirements

Requirements are (in decreasing order of importance):
  • Familiarity with functional programming, e.g. OCaml, Haskell or Scala.
  • Experience with the Coq proof assistant.
  • Familiarity with the extraction mechanism of Coq is a plus.
  • Having some elementary notions of web programming is a plus.
Further reading
  • FA1.2: Approvable Ledger Interface
  • FA1.2 Approvable Ledger, formal verification by Nomadic Labs
  • Formal Verification of ERC20 Contracts
  • ERC20 Token Verifier

Internship Context

You will work at the Nomadic Labs’ offices in Paris.
Participating in a large scale open-source project you will have to rapidly learn to use collaborative tools (Git, merge request, issues, gitlab, continuous integration, documentation) and to communicate about your work. The final results might be presented at an international conference or workshop.
You will have a designated advisor at Nomadic Labs and will have to work independently and to propose thoroughly-considered solutions to the different problems you will have to solve. You will be encouraged to seek advice from members of the team.

Intellectual Property

All material produced (essays, documentation, code, etc.) will be released under an open source license (e.g. MIT or CC).

➡️ If you don’t meet all the criteria above, but think you can still be an asset to us, please consider applying.