We are experts with PhDs specializing in programming languages design and compilation, in particular on the OCaml language (profiling, etc.).
We have contributed to different software in this domain such as the OCaml memory profiler, js_of_ocaml, etc. We have applied our expertise in the blockchain world with contribution to the smart language Michelson in the Tezos node, and the high level language Liquidity with its compiler to and from Michelson.
Six years of experience developing blockchains and applications.
We have taken part in the development of public blockchains (Tezos node, smart contract languages) and have built open source private blockchain instances with on-demand extensions. This work is complemented by tooling such as block explorers, IDEs, remote proxy signers, ... We have also built numerous blockchain-based systems and decentralized applications.
We are experts in automated reasoning and model checking, and the principal contributors to several tools like the SMT solver Alt-Ergo and the parameterized model checker Cubicle. We have also contributed to the model checker Kind2, or the formally verified SMTCoq plugin which allows to use SMT solvers in Coq.
We have published more than 20 research papers in the top international conferences on formal methods (CAV, IJCAR, TACAS, FM, FMCAD, NFM, etc.)
We deliver custom, safe, and secure solutions (from POC/MVC to a final product deployment) and help bring your ideas to life.
We identify, analyze, and discuss with you the appropriate solution(s) for your need.
We like sharing our experience and expertise of blockchains, formal methods and OCaml. We can help your team better understand the ins and outs of blockchain technology.