diff --git a/Technology b/Technology
index 2c2e94c..cb76142 100644
--- a/Technology
+++ b/Technology
@@ -142,8 +142,7 @@ module interface.
 ### Verification
 
 A large subset of the OCaml semantics has been
-[mechanized](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover, and
-this metatheory is verified.
+[mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover.
 
 OCaml is the implementation language of the well-known proof assistant
 [Coq](https://coq.inria.fr).  Development in Coq can be extracted to OCaml code,