Inria, the French National Institute for computer science and applied mathematics, is a world-class research institution and a main developer of core technologies used in the Tezos protocol, such as OCaml and Coq. Its researchers have been developing OCaml, the functional programming language used to implement Tezos, for several decades. It also created Coq, a proof assistant, to help ensure the correctness of programs, which may be used to formally verify key parts of the Tezos protocol as well as smart contracts.
With the Foundation’s support, Inria will focus on research and other efforts that include: cryptography and cybersecurity, distributed systems, research and development of the OCaml language, formal verification and proofs, and other related technologies. The additional resources provided by the Foundation will allow Inria to establish several internal labs, staff full-time research teams, and generally strengthen their involvement in applications that relate to blockchain technology.
Furthermore, the Tezos Foundation is excited to support Tarides, a Paris-based company led by Thomas Gazagnaire (formerly Citrix, Unikernel Systems, and Docker). Tarides’ research will focus on packaging Tezos as a MirageOS unikernel, which will help participants establish nodes on the Tezos network in a more efficient and secure manner. Lastly, the Tarides team includes authors of the MirageOS unikernel project and has a strong background in both academia and industry.
The Tezos Foundation is committed to funding relevant research and projects that will support and benefit the Tezos protocol, and is pleased to support these exceptional groups. It has previously announced its support of IMDEA Software Institute, OCaml Labs, Obsidian Systems, and the Learn OCaml project.