
<!-- Link definitions  -->
[Alt-Ergo]: https://alt-ergo.ocamlpro.com
[Why3]: http://why3.lri.fr
[Frama-C]: https://frama-c.com
[SPARK]: https://www.adacore.com/sparkpro
[Common Criteria]: https://www.commoncriteriaportal.org/
[B]: https://www.atelierb.eu/
[CEA List]: http://www-list.cea.fr/
[MERCE]: https://www.mitsubishielectric-rce.eu/
[INRIA]: https://www.inria.fr/fr
[Adacore]: https://www.adacore.com/
[TrustInSoft]: https://trust-in-soft.com/
[Dolmen]: https://github.com/Gbury/dolmen

# Formal Methods


<!-- [JB] Only content for now. Maybe add an intro ? -->

## Alt-Ergo

[Alt-Ergo] is an open-source automatic solver
based on Satisfiability Modulo Theories (SMT). Successfully designed for 
proving formulas generated in the
context of deductive program verification.

It is mostly used as a back-end of different program verification tools via
the [Why3] platform like [Frama-C]
for C or [SPARK] for Ada. [Alt-Ergo] is also used
to prove formulas issued from [B] modelizations and from cryptographic protocols
verification. 

Commercial usage is allowed by joining the [Alt-Ergo] club which is a way for
the [Alt-Ergo] team to get closer to their users, collect their needs, 
integrate them in the [Alt-Ergo] roadmap, and ensure sustainable funding for
this project's long-term development.

## Program Verification

We developped several static analysis enforcing security or safety properties
in various languages:
- safety requirements in C <!-- [JB] can we mention MERCE and/or the related project? -->
- OCaml exceptions tracking <!-- [JB] add SecureOCaml FUI link? -->
- reaching unspecified or breaking invariant states in transition system based languages <!-- [JB] GEHC is under NDA so we can't talk explicitly about it but we may link to mikino/verification for dummies. -->

## Certification

High assurance level in [Common Criteria] certification implies the formalization
of at least the security policy model corresponding to the family SPM. Such 
formalization is usually expensive and subcontracting it lower both the risk 
and costs.

Our experienced R&D team can deal with it and help your products reaching the
EAL 6 or 7 certification.

## Partnership

We are involved in formal methods related partnership:
- [INRIA]
- [CEA List]
- [MERCE]
- [Adacore]
- [TrustInSoft]
- <!-- [JB] More ?-->

In addition, we contribute to open-source tooling:
- [Dolmen]: a generic front-end for solvers
- <!-- [JB] What else ? -->