diff --git a/Home b/Home
index 2d75f94..161c1bd 100644
--- a/Home
+++ b/Home
@@ -17,7 +17,7 @@ With our approach to systems development we provide the following advantages for
 * minimal codebase without mutable state allows to reason about entire systems and adherence to specification
 * extensive library ecosystem, yet minimal trusted code base at runtime
 * rapid prototyping with a seamless path from prototype to production
-* possibility to formally verify important parts with a therorem prover
+* possibility to formally verify important parts with a proof assistant
 
 
 Our team is eager to develop applications for high assurance, which seamlessly
diff --git a/Technology b/Technology
index 2bb9c20..eff1e58 100644
--- a/Technology
+++ b/Technology
@@ -144,8 +144,8 @@ module interface.
 
 ### Verification
 
-A large subset of the OCaml semantics has been
-[mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover.
+A large subset of the OCaml semantics has been [mechanically proven
+sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a proof assistant.
 
 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,