diff --git a/Technology b/Technology
index 5d938c9..2bb9c20 100644
--- a/Technology
+++ b/Technology
@@ -153,6 +153,9 @@ as demonstrated by [compcert](http://compcert.inria.fr/), a formally verified
 optimizing C compiler, in order to be compiled and executed.  The other
 direction is also possible: OCaml code can be translated into Coq definitions
 (using [Coq of OCaml](https://github.com/clarus/coq-of-ocaml/)).
+[CFML](http://www.chargueraud.org/softs/cfml/) is an ongoing research project
+which enables us to prove properties about OCaml programs using the
+[Coq](https://coq.inria.fr) proof assistant.
 
 The National Cybersecurity Agency of France reviewed the implementation of the
 OCaml runtime system, [their