<h4>Other achievements in Formal Methods and DSLs/Programming Language Expertise</h4>
-[tzscan](https://tzscan.io/), the Tezos network explorer
-[Liquidity](https://www.liquidity-lang.org/), a smart-contract language for the Tezos blockchain
-[OPTAL](https://github.com/OcamlPro/optal), Language for Linear Optimization
-[memprof](http://memprof.typerex.org/), non-intrusive memory profiler for OCaml applications
-[Techelson](https://ocamlpro.github.io/techelson/), a test execution engine for Michelson
-[TryOCaml](https://try.ocamlpro.com/), Online top-level for beginners
<hrclass="featurette-divider">
<hrclass="featurette-divider">
<h2class="page-subtitle">You're in good company</h2>
<h2>
Project with <ahref="https://www.mitsubishielectric-rce.eu/">Mitsubishi Electric R&D Centre Europe</a>
</h2>
<p>
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.
</p>
<figureclass="quote">
<blockquoteclass="text-end">
<p>
“MERCE was very satisfied of OCamlPro. The project was technically challenging and time constrained, nonetheless OCamlPro met the requirements in time while producing a code of excellent quality.”
</p>
<figcaptionclass="blockquote-footer">
David Mentré, <cite>MERCE</cite>
</figcaption>
</blockquote>
</figure>
<hrclass="featurette-divider">
<h1class="page-subtitle"align="center">You're in good company</h1>
<br/>
<br/>
<br/>
<br/>
...
@@ -147,3 +155,72 @@ We cater to very specific needs. For example, we can translate a “black box”
...
@@ -147,3 +155,72 @@ We cater to very specific needs. For example, we can translate a “black box”
<h2class="page-subtitle">Sharing our expertise with you: Consulting & Training</h2>
<br/>
Our developments are harnessing our expertise on formal methods and the most advanced features of OCaml & Rust. We will help you design robust architectures, choose open-source components, optimize your code and solve performance, memory or compiler issues.
We also support companies that need to get up to speed, with on-demand and customized training designed by our experts.
<br/>
<h3>
Open Source tooling to armour industrial developers
</h3>
<br/>
OCamlPro promotes the use of the OCaml functional programming language in the industry, as a token of development productivity and software quality.
We develop and maintain open source tooling for OCaml, such as Opam, [TryOCaml](https://try.ocamlpro.com/), [ocp-indent](https://github.com/OCamlPro/ocp-indent/), [ocp-index](https://github.com/OCamlPro/ocp-index), and ocp-browser.
We contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. We provided a set of tools to foster OCaml adoption, under the legacy TypeRex codename. From the very beginning, we aimed both simplicity of access and perenity.
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 <ahref="https://timelines.cc/view/?timeline=OCamlPro-79628013496459772182883406522017809865">an exhaustive Timeline of OCamlPro’s story</a> of which you can find a small excerpt below.
