diff --git a/src/developers/compiler.md b/src/developers/compiler.md
index 6ab3e0b..48a8dde 100644
--- a/src/developers/compiler.md
+++ b/src/developers/compiler.md
@@ -5,7 +5,7 @@
 ![Hacspec compiler architecture](hacspec_architecture.png)
 
 The Rustspec compiler intervenes after the regular Rust typechecking,
-and takes the Rust AST to translate it into a stricter hacspec AST,
+by translating the Rust AST into a stricter hacspec AST,
 yielding error messages if you're not in the subset.
 
 The hacspec AST then undergoes a typechecking phase that replicates the
@@ -34,7 +34,7 @@ building the AST.
 ### Translation from Rust AST
 
 This phase is contained in `ast_to_rustspec.rs`. The trickyness of this
-translation is that it needs o be aware of certain special names contained
+translation is that it needs to be aware of certain special names contained
 in the structure `SpecialNames`. Indeed, while the Rust AST treats the application
 enum constructors like function applications, the hacspec AST considers them as
 proper injection so we need to distinguish them in the Rust AST. For that, we
@@ -65,7 +65,7 @@ and global variables from each other.
 
 ### External data
 
-A hacspec file can never almost never be considered alone, as it usually imports
+A hacspec file can never (in principal) be considered alone, as it usually imports
 at least several other crates like the hacspec standard library. These external
 crates must pre-populate the typechecking context with the types and function
 signatures that they define.
@@ -144,7 +144,7 @@ assistant libraries.
 
 ## Unit tests
 
-The compiler has various unit tests that are control trough the `language/tests`
+The compiler has various unit tests that are controlled trough the `language/tests`
 files. Please enrich the unit tests bases in `language-tests`,
 `negative-language-tests` and `test-crate` as you implement new features for
 the compiler. The compiler can also be tested against all the hacspec cryptographic
diff --git a/src/std/arithmetic.md b/src/std/arithmetic.md
index 7216653..43b116a 100644
--- a/src/std/arithmetic.md
+++ b/src/std/arithmetic.md
@@ -23,7 +23,7 @@ let y: u64 = 4u64; // GOOD
 
 ## Public and secret integers
 
-One of hacspec's goal is to enable users quickly check whether their
+One of hacspec's goal is to enable users to quickly check whether their
 application does not obviously break the constant-time guarantee.
 Certain processor instructions take more or less time to complete depending
 on their inputs, which can cause secret leakage and break the security of
diff --git a/src/std/seq.md b/src/std/seq.md
index 02d4d0a..319f3d5 100644
--- a/src/std/seq.md
+++ b/src/std/seq.md
@@ -1,13 +1,10 @@
 # Sequence and array operations
 
-While the types for [sequence and arrays](/language/seq.md) has been introduced
-earlier,
-
 ## Operations common to sequences and arrays
 
 ### Base traits
 
-Some operations are common to both [sequences and arrays](/language/seq.md)
+Some operations are common to both [sequences and arrays](/book/language/seq.md)
 by design, and can be used as the interoperability base between the two types
 of collections. These operations are the following:
 * `len`: gives the length of an array or sequence;
@@ -46,7 +43,7 @@ data under the hood.
 
 ### Ownage
 
-Some mehtods have two versions: an `owned` and a non-`owned` version, depending
+Some methods have two versions: an `owned` and a non-`owned` version, depending
 on whether the `self` argument is consumed or not by the method. This distinction
 is useful to avoid unnecessary copies and thus be more performant.
 
diff --git a/src/usage/verification.md b/src/usage/verification.md
index 0f3bbd7..d7ae51f 100644
--- a/src/usage/verification.md
+++ b/src/usage/verification.md
@@ -4,7 +4,7 @@
 
 ### QuickCheck / QuickChick
 
-You can test your hacspec code using quickcheck, simply implmenet Arbitrary for the type you want to generate tests for, e.g.
+You can test your hacspec code using [QuickCheck](https://github.com/BurntSushi/quickcheck) (a Rust library for randomized property-based testing), by simply implementing `quickcheck::Arbitrary` for the type you want to generate tests for. For example:
 ```rust,ignore
 impl Arbitrary for Fp {
     fn arbitrary(g: &mut Gen) -> Fp {
@@ -21,7 +21,7 @@ impl Arbitrary for Fp {
     }
 }
 ```
-then you can use the QuickCheck attribute, to make QuickCheck do property based testing for this function,
+then you can use the `quickcheck` attribute, to make QuickCheck do property based testing for this function:
 ```rust,ignore
 #[cfg(test)]
 #[quickcheck] //Using the fp arbitraty implementation from above to generate fp2 elements.
@@ -34,7 +34,7 @@ which will run when you do `cargo test`. If you then add the tag `#[cfg(proof)]`
 ```
 cargo hacspec -o coq/src/<output_file_name>.v <input_crate_name>
 ```
-then you get the QuickChick test,
+then you get corresponding [QuickChick](https://github.com/QuickChick/QuickChick) test,
 ```
 Definition test_fp2_prop_add_neg (a_320 : fp2) : bool :=
   let b_321 :=