Company.
Functori was founded in February 2021 in the Paris region, by engineers coming from academic research. We are about eleven people today, five of them PhDs.
Who we are
Five founders who came to blockchains from research in programming languages and formal methods.
Before Functori, we built and published tools for checking software: the Alt-Ergo SMT prover, the Cubicle and Kind model checkers, memory profiling for OCaml. That work was done at Université Paris-Saclay, École polytechnique, OCamlPro and the University of Iowa.
We still work that way: OCaml, Rust, Solidity and TypeScript, typed and tested code, and a proof when a piece of the system has to be right.
How we work
Research-driven engineering
Five of us hold a PhD. We coordinate the Argos consortium and lead a work package of CryptoACTION.
We build our own tools
Explorus, Mitten, Apollo and EVM TxRay: tools we built for our projects and still use.
Open source
Our libraries, from Tzfunc to Vue PPX, are on our GitLab.
Close to academia
An industrial PhD with LIP6 (Sorbonne Université), and research ties with LMF, IRILL and Universidade do Algarve.
We write about our work
25 articles on our blog since 2022, and talks at JFLA.
Engineers first
Clients work directly with the engineers who write their code.
Since 2021
We started with client engineering and one venture. Research projects came later, and Argos came out of them.
2021
Functori is founded in the Paris region. Our engineers start working on the core of Tezos with Nomadic Labs, and we become technical co-founder of Fraktion.
2022
Tenderbake, the consensus we reviewed and formalized, goes live on Tezos. The Tezos Foundation funds Explorus, our consensus explorer, and we present Mitten, our consensus scenario tool, at JFLA.
2023
Smart Rollups go live on Tezos, with our work on the rollup node and refutation proofs. The Argos consortium starts, funded by Bpifrance and coordinated by Functori.
2024
We design and implement the Etherlink rollup, kernel and node, with Trilitech.
2025
CryptoACTION, a Horizon Europe project, starts. We lead its crypto-transaction analysis work package.
2026
One of Argos's detection algorithms is machine-checked in Rocq and evaluated on 220,000 Ethereum blocks. An industrial PhD with LIP6 (Sorbonne Université) starts, on exploring transaction graphs.
Founders
Çağdaş Bozman
OCamlMemory profiling
PhD from École polytechnique on memory profiling for OCaml.
Mohamed Iguernlala
SMT solvingAutomated reasoningFormal verification
PhD from Université Paris-Saclay on SMT solving; long-time contributor to the Alt-Ergo prover.
Alain Mebsout
Model checkingSMTFormal verification
PhD from Université Paris-Saclay on model checking (Cubicle); postdoctoral research at the University of Iowa (Kind).
Maxime Levillain
ProductFunctional programmingTooling
PhD from Université Paris-Saclay in hadronic physics.
Michael Laporte
DeFiBlockchain protocols
MSc from Université Paris-Diderot.
Contact
Write to contact@functori.com, or pick your topic below.