Our open source software
OCamlPro has a record of outstanding technological achievements and success stories, in areas from web tools to distributed frameworks, DSLs and formal methods. 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.
Some projects showcasing our areas of expertise:
- Owi: we developed OWI, an interpreter for WebAssembly designed for experimentation and analysis, with support for concolic execution and formal reasoning Owi - Symbolic execution for Wasm, C, C++, Rust and Zig. Our goal was to experiment with Wasm GC proposals, as part of our involvement in this working group;
- Flambda: we developed Flambda, an highly optimizing compiler for OCaml, focusing on aggressive inlining, specialization, and performance improvements. This compiler is used by Jane Street Capital, one of the top HFT trading firms in the world;
- Wasocaml: we developed Wasocaml, a toolchain for compiling OCaml code to WebAssembly, enabling strong integration between high-level functional code and low-level execution environments (submitted as a prototype to the Wasm GC WG)
- Decysif: we participate in the Decysif project, a state funded multiyear project with academic and industrial partners to formally verify Rust code, combining static analysis and formal methods to secure embedded or critical systems. Partners include Trust in Soft and Adacore;
- EAL6+ formal verification: we have successfully verified in Coq several bootloaders for Samsung at EAL6+ certification level of Common Criteria, so that they can be commercialized on European markets;
- About our SMT Solver Alt-Ergo and its Club and other Formal Methods related topics, there are a few blogposts.
We also contribute on
