Harnessing Cutting-Edge Technologies
State-of-the-art languages for modern solutions
We have years of experience on the research and development of programming languages, formal methods techniques and tools as well as their application in industrial settings. Let’s achieve bold projects together!
For industrial partners who face challenges
For R&D labs who need collaboration
For developers to reach mastery
Prototyping software solutions for you
We design and implement reliable high-value solutions for our clients. As a challenge-driven team, we can find with you the most elegant and efficient solutions to optimize your products or create new ones.
OCamlPro has a record of outstanding technological achievements and success stories, in areas from web tools to distributed frameworks, DSLs and formal methods. We also built a strong blockchain expertise since 2014 on the Tezos and Dune Network blockchains. Developments are done in OCaml or Rust, and then integrated with other software in any language (C, C++, Python, Java, etc.). Our applications are extensible and maintainable, fully independent from web servers, portable to all mainstream browsers.
We cater to very specific needs. For example, we can translate a “black box” application from a programming language (Go, Coq, Cobol…) to a comprehensive language for your current team. Whether an ex-employee or a contractor coded everything in a language your current team hasn’t mastered, or it’s running on a legacy language, we can provide assistance.
A highly scalable package manager
Exercise platform for teachers and learners around the world aiming to discover OCaml
An SMT solver for software verification
A blockchain with integrated governance
A Solidity Parser in OCaml with Menhir
A language for linear optimisation
Other achievements in Formal Methods and DSLs/Programming Language Expertise
- tzscan, the Tezos network explorer
- Liquidity, a smart-contract language for the Tezos blockchain
- OPTAL, Language for Linear Optimization
- memprof, non-intrusive memory profiler for OCaml applications
- Techelson, a test execution engine for Michelson
- TryOcaml, Online top-level for beginners
Project with Mitsubishi Electric R&D Centre Europe
Starting from a specification provided by MERCE, we designed and implemented a formal verification analysis tool to check a particular class of safety properties over C programs. The tool was implemented as a Frama-C plug-in and came with fully fledged user and formal documentation.
You're in good company
Discover our timeline
Months and months of lockdown have allowed us to take the time to look back on events of the past years and to advertise our strong ties with academic and industrial partners, and our achievements through a comprehensive Timeline of OCamlPro’s story of which you can find a small excerpt below.
- April 1, 2011
- OCamlPro is founded
- OCamlPro is founded to help spread the OCaml language in the industry.
Fabrice le Fessant, a researcher and member of the French Inria Institute, founds OCamlPro to boost the development of OCaml and promote it in the industry.
- July 1, 2015
- Paris 7 appoints OCamlPro to implement the exercise platform of the OCaml MOOC on France Université Numérique
- OCamlPro implements the first version of the exercise autocorrecting platform of the OCaml MOOC on FUN for Paris 7, based on TryOCaml, integrates to the OpenEDX/FUN and designs some of the exercices of the course, in collaboration with Roberto Di Cosmo and Yann-Régis Gianas (Irill).
- November 1, 2016
- Alt-Ergo 1.30 release with experimental support for model generation
- Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.
- February 14, 2020
- Alt-Ergo Users' Club: MERCE (Mitsubishi Electric Research Centre in Europe) and Why3 join the Club
- The second annual meeting of the Alt-Ergo Users' Club was held in mid-February. These meetings are the perfect place to review each partner's needs regarding Alt-Ergo, discuss the roadmap for future Alt-Ergo developments and enhancements.