The Tezos Foundation, the overseer of the Tezos blockchain protocol, announced today that it has issued grants to Kyoto University and Edukera, based in Japan and France, respectively, to further advance the Tezos smart contract development ecosystem.

Kyoto University

Kyoto University is the second oldest Japanese university and one of Asia’s leading research institutions with 18 Nobel laureates, more than any other university in Asia. With this grant, Kyoto University has conducted research on the current, simple Michelson type-checking to develop static verification techniques for Michelson and higher-level Tezos smart contract languages.

Led by Atsushi Igarashi, Ph.D., a professor at the Graduate School of Informatics, and Kohei Suenaga, Ph.D., an associate professor at the Graduate School of Informatics, the team will create an accessible development tool for these verification techniques and contribute to the growth of the Tezos ecosystem in Japan and the greater Asia region. Jun Furuse of DaiLambda and Tezos Japan collaborates with Kyoto University on this project.


Edukera is an online application to teach formal logic and math. Founded in 2013 by Benoit Rognier and Guillaume Duhamel, the team has a proven ability to provide the public with learning solutions based on the Coq proof assistant.

Led by scientific director Pierre-Yves Strub, an assistant professor at and Ph.D. recipient in Computer Science of École Polytechnique in Paris, France, the Edukera team has formally verified properties of several Tezos smart contracts and begun development of a new Tezos smart contracts language, Archetype.

Archetype is a domain-specific language to develop smart contracts on Tezos, with a specific focus on more easily facilitating formal verification.