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!
We have an outstanding expertise in programming languages, theory, design, compilation, profiling, DSLs, and a lot of development.
We have years of practice in the development of programs and tooling for many programming languages, such as Rust and OCaml advanced functional languages, Solidity and Michelson for smart contracts, and even COBOL and other legacy languages.
Most of our developers are PhD-level experts in formal specification and automated verification of programs and smart contracts.
We have a huge experience in specification, audit and verification of systems and programs. We maintain the Alt-Ergo automatic SMT solver within the Alt-Ergo Users' Club. We have experience in formal modeling that is relevant for EAL6+ certification with tools like Coq.
We are part of the Everscale Formal Methods sub-governance, in charge of auditing and verifying Solidity smart contracts.
Blockchain & Distribution
We have more than twenty years of experience in the design of distributed systems and the development of blockchains.
We design blockchain applications using the most advanced technologies, such as Avalanche and Everscale. Since 2014, we developed the prototype of the Tezos blockchain, its ICO infrastructure, the TzScan block-explorer, the Michelson to Liquidity decompiler, the Ironmin storage layer and many other tools to easily interact with the most complex blockchain environments. We develop and audit smart contracts in various programming languages, such as Solidity or Michelson.
Professional services for demanding customers
Consulting and Training
You are starting an ambitious project ? We can team up with you to analyse your project and provide the best technical advices to help you meet your goals.
We have a long experience of software project, from prototyping innovative software to modernization of legacy infrastructures. We always know the expert that you need for any specific domain. We also like to share our knowledge through beginers and experts training in computer fields.
Research & Development
Research and innovation is in our DNA. We enjoy solving challenging problems using our academic backgrounds.
With a large team of PhD-level engineers, we are involved in many research projects, and always looking for new ones to solve! We are labelled as a private research lab for French CIR for direct contracts, and we also enjoy partnering through collaborative national or european R&D projects.
Audit and Certification
With an outstanding expertise in software development and formal verification, we are able to audit any software and provide certification using formal methods.
We audit and verify critical software systems in most programming languages, from smart contracts written in languages such as Solidity or Michelson, to cybersecurity systems that must conform to Common Criteria at EAL6 and more levels.
OCaml and Rust Development
We use the most reliable and performant technologies to develop the software that you really want.
We always choose the best programming language for the solution that we have to develop: we often use OCaml, because it is the most expressive (far more than Python for example), yet with a modern type-system and C-like performance. It made us one of the top open-source contributors in the OCaml ecosystem. For performance-critical applications, we often switch to Rust, that provides astonishing speed.
We develop complete and reliable web3 applications for any blockchain technology, in a timely manner.
We have been in the blockchain space for a longer time than most other companies, developing projects from blockchain core protocols to full web3 applications for various blockchains, such as Everscale, Avalanche and Tezos. Every new project is an opportunity to learn and use our skills in a domain full of disruptions. We are currently working on projects around DeFi, NFTs, etc.
We have a unique way to work with startups, as techno-founders, investing not money but technology!
We enjoy meeting startups and discovering their projects, often providing insightful advices. Sometimes, we like a project so much that we decide to invest in it: many startups need developers more than they need funds, so that's what we provide to them! Our highly-experienced team is a real assets to meet your market on time!
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.
We have a set of other dedicated websites:
- Rust Expertise: rust-coders.com, rust-expertise.com, red-iron.eu, iron-red.com
- Rust Expertise (in French): rust-coders.fr, rust-expertise.fr, red-iron.fr, iron-red.fr, rust-experts.fr
- Cobol Expertise: cobol-expertise.com
- Cobol Expertise (in French): cobol-expertise.fr
- Training: training.ocamlpro.com