diff --git a/docs/reference/evercrypt/dh/ec/index.md b/docs/reference/evercrypt/dh/ec/index.md
index 60016029..efcfcc8a 100644
--- a/docs/reference/evercrypt/dh/ec/index.md
+++ b/docs/reference/evercrypt/dh/ec/index.md
@@ -2,12 +2,14 @@
 
 Elliptic-curve Diffie-Hellman key agreement on Curve25519.
 
-## API Reference
+## Available Implementations
 
 ```C
 #include "EverCrypt_Curve25519.h"
 ```
 
+## API Reference
+
 ```{doxygenfunction} EverCrypt_Curve25519_scalarmult
 ```
 
diff --git a/docs/reference/evercrypt/randomness/index.md b/docs/reference/evercrypt/randomness/index.md
index 46970966..c5f84beb 100644
--- a/docs/reference/evercrypt/randomness/index.md
+++ b/docs/reference/evercrypt/randomness/index.md
@@ -4,12 +4,14 @@
 
 Deterministic Random Bit Generator (DRBG) (NIST, SP 800-90A).
 
-### API Reference
+## Available Implementations
 
 ```C
 #include "EverCrypt_DRBG.h"
 ```
 
+### API Reference
+
 #### Variables
 
 ```{doxygenvariable} EverCrypt_DRBG_reseed_interval
diff --git a/docs/reference/hacl/aead/chacha20poly1305.md b/docs/reference/hacl/aead/chacha20poly1305.md
index fe0e659d..69cb497d 100644
--- a/docs/reference/hacl/aead/chacha20poly1305.md
+++ b/docs/reference/hacl/aead/chacha20poly1305.md
@@ -1,12 +1,7 @@
 # Chacha20-Poly1305
 
 HACL implements the Chacha20-Poly1305 Authenticated Encryption with Associated Data (AEAD) construction specified in [RFC 8439].
-The library includes three implementations of this construction, all with the same API, for different platforms:
-
-* `Hacl_Chacha20Poly1305_32.h` contains the API for the portable C implementation that can be compiled and run on any platform that is 32-bit or higher.
-* `Hacl_Chacha20Poly1305_128.h` contains the API for the 128-bit vectorized C implementation that can be compiled and run on any platform that supports 128-bit SIMD instructions.
-* `Hacl_Chacha20Poly1305_256.h` contains the API for the 256-bit vectorized C implementation that can be compiled and run on any platform that supports 256-bit SIMD instructions.
-
+The library includes three implementations of this construction, all with the same API, for different platforms.
 All memory for the output variables have to be allocated by the caller.
 
 ## Available Implementations
@@ -18,6 +13,8 @@ All memory for the output variables have to be allocated by the caller.
 #include "Hacl_Chacha20Poly1305_32.h"
 ```
 
+A portable C implementation that can be compiled and run on any platform that is 32-bit or higher.
+
 This implementation works on all CPUs.
 ````
 
@@ -26,6 +23,8 @@ This implementation works on all CPUs.
 #include "Hacl_Chacha20Poly1305_128.h"
 ```
 
+A 128-bit vectorized C implementation that can be compiled and run on any platform that supports 128-bit SIMD instructions.
+
 Support for VEC128 is needed. Please see the [HACL Packages book].
 ````
 
@@ -34,11 +33,17 @@ Support for VEC128 is needed. Please see the [HACL Packages book].
 #include "Hacl_Chacha20Poly1305_256.h"
 ```
 
+A 256-bit vectorized C implementation that can be compiled and run on any platform that supports 256-bit SIMD instructions.
+
 Support for VEC256 is needed. Please see the [HACL Packages book].
 ````
 `````
 
-## Example
+## API Reference
+
+`````{tabs}
+````{group-tab} 32
+**Example**
 
 ```{literalinclude} ../../../../tests/chacha20poly1305.cc
 :language: C
@@ -47,55 +52,30 @@ Support for VEC256 is needed. Please see the [HACL Packages book].
 :end-before: "// END OneShot"
 ```
 
-## API Reference
-
-`````{tabs}
-
-````{group-tab} 32
-
 ```{doxygenfunction} Hacl_Chacha20Poly1305_32_aead_encrypt
 ```
-
-````
-
-````{group-tab} 128
-
-```{doxygenfunction} Hacl_Chacha20Poly1305_128_aead_encrypt
-```
-
-````
-
-````{group-tab} 256
-
-```{doxygenfunction} Hacl_Chacha20Poly1305_256_aead_encrypt
-```
-
-````
-`````
-
--------------------------------------------------------------------------------
-
-`````{tabs}
-
-````{group-tab} 32
-
 ```{doxygenfunction} Hacl_Chacha20Poly1305_32_aead_decrypt
 ```
-
 ````
-
 ````{group-tab} 128
+**Example**
 
+There is no example for now.
+
+```{doxygenfunction} Hacl_Chacha20Poly1305_128_aead_encrypt
+```
 ```{doxygenfunction} Hacl_Chacha20Poly1305_128_aead_decrypt
 ```
-
 ````
-
 ````{group-tab} 256
+**Example**
+
+There is no example for now.
 
+```{doxygenfunction} Hacl_Chacha20Poly1305_256_aead_encrypt
+```
 ```{doxygenfunction} Hacl_Chacha20Poly1305_256_aead_decrypt
 ```
-
 ````
 `````
 
diff --git a/docs/reference/hacl/dh/ec/curve25519.md b/docs/reference/hacl/dh/ec/curve25519.md
index ee544643..0d5e098e 100644
--- a/docs/reference/hacl/dh/ec/curve25519.md
+++ b/docs/reference/hacl/dh/ec/curve25519.md
@@ -2,34 +2,34 @@
 
 Elliptic-curve Diffie-Hellman key agreement on Curve25519.
 
-## Implementations
-
-There are multiple implementations, i.e., ...
-
-* a portable implementation (`Hacl_Curve25519_51.h`),
-* a fast 64-bit implementation that requires BMI2 & ADX CPU support (`Hacl_Curve25519_64.h`), and
-* a slower 64-bit implementation without the requirements stated above (`Hacl_Curve25519_64_Slow.h`).
-
-## API Reference
+## Available Implementations
 
 `````{tabs}
 ````{group-tab} 51
 ```C
 #include "Hacl_Curve25519_51.h"
 ```
+
+A portable implementation.
 ````
 ````{group-tab} 64
 ```C
 #include "Hacl_Curve25519_64.h"
 ```
+
+A fast 64-bit implementation that requires BMI2 & ADX CPU support.
 ````
 ````{group-tab} 64 (Slow)
 ```C
 #include "Hacl_Curve25519_64_Slow.h"
 ```
+
+A slow 64-bit implementation without the requirements stated above.
 ````
 `````
 
+## API Reference
+
 `````{tabs}
 ````{group-tab} 51
 ```{doxygenfunction} Hacl_Curve25519_51_scalarmult
diff --git a/docs/reference/hacl/hash/blake2/blake2b.md b/docs/reference/hacl/hash/blake2/blake2b.md
index 0e48631d..2f06c004 100644
--- a/docs/reference/hacl/hash/blake2/blake2b.md
+++ b/docs/reference/hacl/hash/blake2/blake2b.md
@@ -3,10 +3,29 @@
 BLAKE2b is optimized for 64-bit platforms and produces digests of any size between 1 and 64 bytes.
 It also has a build-in keying mechanism so that it can be used to replace HMAC-based constructions.
 
-## Example
+## API Reference
+
+### One-Shot
+
+**Available Implementations**
+
+`````{tabs}
+````{group-tab} 32
+```C
+#include "Hacl_Hash_Blake2.h"
+```
+````
+````{group-tab} 256
+```C
+#include "Hacl_Hash_Blake2b_256.h"
+```
+````
+`````
 
-The following example shows how to use the one-shot API with the base implementation (32) of BLAKE2b.
+**Example**
 
+`````{tabs}
+````{group-tab} 32
 ```{literalinclude} ../../../../../tests/blake2b.cc
 :language: C
 :dedent:
@@ -27,24 +46,18 @@ The following example shows how to use the one-shot API with the base implementa
 :start-after: "// ANCHOR(example)"
 :end-before: "// ANCHOR_END(example)"
 ```
-
-## API Reference
-
-### One-Shot
+````
+````{group-tab} 256
+There is no example for now.
+````
+`````
 
 `````{tabs}
 ````{group-tab} 32
-```C
-#include "Hacl_Hash_Blake2.h"
-```
-
 ```{doxygenfunction} Hacl_Blake2b_32_blake2b
 ```
 ````
 ````{group-tab} 256
-```C
-#include "Hacl_Hash_Blake2b_256.h"
-```
 ```{doxygenfunction} Hacl_Blake2b_256_blake2b
 ```
 ````
@@ -52,6 +65,7 @@ The following example shows how to use the one-shot API with the base implementa
 
 ### Streaming (without key)
 
+**Available Implementations**
 
 `````{tabs}
 ````{group-tab} 32
@@ -66,69 +80,44 @@ The following example shows how to use the one-shot API with the base implementa
 ````
 `````
 
+**Example**
+
 `````{tabs}
 ````{group-tab} 32
-```{doxygentypedef} Hacl_Streaming_Blake2_blake2b_32_state
-```
+There is no example for now.
 ````
 ````{group-tab} 256
-```{doxygentypedef} Hacl_Streaming_Blake2b_256_blake2b_256_state
-```
+There is no example for now.
 ````
 `````
 
 `````{tabs}
 ````{group-tab} 32
-```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_create_in
+```{doxygentypedef} Hacl_Streaming_Blake2_blake2b_32_state
 ```
-````
-````{group-tab} 256
-```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_create_in
+```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_create_in
 ```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_init
 ```
-````
-````{group-tab} 256
-```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_init
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_update
 ```
-````
-````{group-tab} 256
-```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_update
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_finish
 ```
-````
-````{group-tab} 256
-```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_finish
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2b_32_no_key_free
 ```
 ````
 ````{group-tab} 256
+```{doxygentypedef} Hacl_Streaming_Blake2b_256_blake2b_256_state
+```
+```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_create_in
+```
+```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_init
+```
+```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_update
+```
+```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_finish
+```
 ```{doxygenfunction} Hacl_Streaming_Blake2b_256_blake2b_256_no_key_free
 ```
 ````
 `````
-
diff --git a/docs/reference/hacl/hash/blake2/blake2s.md b/docs/reference/hacl/hash/blake2/blake2s.md
index ff1a5edd..e333ef9d 100644
--- a/docs/reference/hacl/hash/blake2/blake2s.md
+++ b/docs/reference/hacl/hash/blake2/blake2s.md
@@ -2,10 +2,29 @@
 
 BLAKE2s is optimized for 8- to 32-bit platforms and produces digests of any size between 1 and 32 bytes.
 
-## Example
+## API Reference
+
+### One-Shot
 
-The following example shows how to use the one-shot API with the base implementation (32) of BLAKE2s.
+**Available Implementations**
 
+`````{tabs}
+````{group-tab} 32
+```C
+#include "Hacl_Hash_Blake2.h"
+```
+````
+````{group-tab} 128
+```C
+#include "Hacl_Hash_Blake2s_128.h"
+```
+````
+`````
+
+**Example**
+
+`````{tabs}
+````{group-tab} 32
 ```{literalinclude} ../../../../../tests/blake2s.cc
 :language: C
 :dedent:
@@ -27,25 +46,18 @@ The following example shows how to use the one-shot API with the base implementa
 :end-before: "// ANCHOR_END(example)"
 ```
 
-## API Reference
-
-### One-Shot
+````
+````{group-tab} 128
+There is no example for now.
+````
+`````
 
 `````{tabs}
 ````{group-tab} 32
-```C
-#include "Hacl_Hash_Blake2.h"
-```
-
 ```{doxygenfunction} Hacl_Blake2s_32_blake2s
 ```
 ````
-
 ````{group-tab} 128
-```C
-#include "Hacl_Hash_Blake2s_128.h"
-```
-
 ```{doxygenfunction} Hacl_Blake2s_128_blake2s
 ```
 ````
@@ -53,6 +65,8 @@ The following example shows how to use the one-shot API with the base implementa
 
 ### Streaming (without key)
 
+**Available Implementations**
+
 `````{tabs}
 ````{group-tab} 32
 ```C
@@ -66,69 +80,44 @@ The following example shows how to use the one-shot API with the base implementa
 ````
 `````
 
+**Example**
+
 `````{tabs}
 ````{group-tab} 32
-```{doxygentypedef} Hacl_Streaming_Blake2_blake2s_32_state
-```
+There is no example for now.
 ````
 ````{group-tab} 128
-```{doxygentypedef} Hacl_Streaming_Blake2s_128_blake2s_128_state
-```
+There is no example for now.
 ````
 `````
 
 `````{tabs}
 ````{group-tab} 32
-```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_create_in
+```{doxygentypedef} Hacl_Streaming_Blake2_blake2s_32_state
 ```
-````
-````{group-tab} 128
-```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_create_in
+```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_create_in
 ```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_init
 ```
-````
-````{group-tab} 128
-```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_init
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_update
 ```
-````
-````{group-tab} 128
-```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_update
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_finish
 ```
-````
-````{group-tab} 128
-```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_finish
-```
-````
-`````
-
-`````{tabs}
-````{group-tab} 32
 ```{doxygenfunction} Hacl_Streaming_Blake2_blake2s_32_no_key_free
 ```
 ````
 ````{group-tab} 128
+```{doxygentypedef} Hacl_Streaming_Blake2s_128_blake2s_128_state
+```
+```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_create_in
+```
+```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_init
+```
+```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_update
+```
+```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_finish
+```
 ```{doxygenfunction} Hacl_Streaming_Blake2s_128_blake2s_128_no_key_free
 ```
 ````
 `````
-
diff --git a/docs/reference/hacl/hash/sha2.md b/docs/reference/hacl/hash/sha2.md
index f60fba92..73cc78c1 100644
--- a/docs/reference/hacl/hash/sha2.md
+++ b/docs/reference/hacl/hash/sha2.md
@@ -18,6 +18,15 @@ it is sometimes called `SHA2-256` to avoid confusion with SHA-1 and SHA-3.
 
 ### One-Shot
 
+**Example**
+
+```{literalinclude} ../../../../tests/sha2.cc
+:language: C
+:dedent:
+:start-after: "// START OneShot"
+:end-before: "// END OneShot"
+```
+
 `````{tabs}
 ````{group-tab} 28 byte digest
 ```{doxygenfunction} Hacl_Hash_SHA2_hash_224
@@ -40,21 +49,17 @@ it is sometimes called `SHA2-256` to avoid confusion with SHA-1 and SHA-3.
 ````
 `````
 
-**Example**
-
-This is an example how to use the SHA-2 one-shot API to digest a complete message.
+### Streaming
 
-The digest is written to the memory pointed to by digest and the caller is expected to allocate enough memory for the digest.
+**Example**
 
 ```{literalinclude} ../../../../tests/sha2.cc
 :language: C
 :dedent:
-:start-after: "// START OneShot"
-:end-before: "// END OneShot"
+:start-after: "// ANCHOR(example streaming)"
+:end-before: "// ANCHOR_END(example streaming)"
 ```
 
-### Streaming
-
 `````{tabs}
 ````{group-tab} 28 byte digest
 
@@ -166,13 +171,3 @@ The digest is written to the memory pointed to by digest and the caller is expec
 ````
 `````
 
-**Example**
-
-```{literalinclude} ../../../../tests/sha2.cc
-:language: C
-:dedent:
-:start-after: "// ANCHOR(example streaming)"
-:end-before: "// ANCHOR_END(example streaming)"
-```
-
-
diff --git a/docs/reference/hacl/hash/sha3.md b/docs/reference/hacl/hash/sha3.md
index a1a926cc..bcf40e87 100644
--- a/docs/reference/hacl/hash/sha3.md
+++ b/docs/reference/hacl/hash/sha3.md
@@ -16,6 +16,15 @@ SHAKE128 and SHAKE256 have a 128- or 256-bit security strength and can produce a
 
 ### One-Shot
 
+**Example**
+
+```{literalinclude} ../../../../tests/sha3.cc
+:language: C
+:dedent:
+:start-after: "// START OneShot"
+:end-before: "// END OneShot"
+```
+
 `````{tabs}
 ````{tab} 28 byte digest
 ```{doxygenfunction} Hacl_SHA3_sha3_224
@@ -38,15 +47,6 @@ SHAKE128 and SHAKE256 have a 128- or 256-bit security strength and can produce a
 ````
 `````
 
-**Example**
-
-```{literalinclude} ../../../../tests/sha3.cc
-:language: C
-:dedent:
-:start-after: "// START OneShot"
-:end-before: "// END OneShot"
-```
-
 ### Streaming
 
 No streaming API available.
@@ -57,6 +57,15 @@ No streaming API available.
 
 #### One-Shot
 
+**Example**
+
+```{literalinclude} ../../../../tests/sha3.cc
+:language: C
+:dedent:
+:start-after: "// ANCHOR(example shake128)"
+:end-before: "// ANCHOR_END(example shake128)"
+```
+
 `````{tabs}
 ````{tab} 128-bit security strength
 ```{doxygenfunction} Hacl_SHA3_shake128_hacl
@@ -69,15 +78,6 @@ No streaming API available.
 ````
 `````
 
-**Example**
-
-```{literalinclude} ../../../../tests/sha3.cc
-:language: C
-:dedent:
-:start-after: "// ANCHOR(example shake128)"
-:end-before: "// ANCHOR_END(example shake128)"
-```
-
 #### Streaming
 
 No streaming API available.
diff --git a/docs/reference/hacl/hazmat/bignum/index.md b/docs/reference/hacl/hazmat/bignum/index.md
index d2e8b1d9..9b6092db 100644
--- a/docs/reference/hacl/hazmat/bignum/index.md
+++ b/docs/reference/hacl/hazmat/bignum/index.md
@@ -10,7 +10,8 @@ HACL's bignum library comes in multiple variants and specializations.
 
 Additional headers: `Hacl_Bignum_Base.h`, `Hacl_Bignum.h`, `Hacl_Bignum25519_51.h`, `Hacl_Bignum_K256.h`.
 
-## API Reference
+
+## Available Implementations
 
 ```````{tabs}
 ``````{group-tab} 32
@@ -53,6 +54,8 @@ Additional headers: `Hacl_Bignum_Base.h`, `Hacl_Bignum.h`, `Hacl_Bignum25519_51.
 ``````
 ```````
 
+## API Reference
+
 ### Loads and stores
 
 ```````{tabs}
diff --git a/docs/reference/hacl/hazmat/montgomery/index.md b/docs/reference/hacl/hazmat/montgomery/index.md
index 2cfade89..da22a4d7 100644
--- a/docs/reference/hacl/hazmat/montgomery/index.md
+++ b/docs/reference/hacl/hazmat/montgomery/index.md
@@ -6,7 +6,7 @@ HACL Packages comes with two versions, a 32-bit optimized version, where bignums
 
 All the arithmetic operations are performed in the Montgomery domain and preserve the invariant that `aM < n` for a bignum `aM` in Montgomery form.
 
-## API Reference
+## Available Implementations
 
 `````{tabs}
 ````{group-tab} 32
@@ -21,6 +21,8 @@ All the arithmetic operations are performed in the Montgomery domain and preserv
 ````
 `````
 
+## API Reference
+
 ### Typedefs
 
 `````{tabs}
diff --git a/docs/reference/hacl/kdf/index.md b/docs/reference/hacl/kdf/index.md
index 35c3fa0b..e8ded810 100644
--- a/docs/reference/hacl/kdf/index.md
+++ b/docs/reference/hacl/kdf/index.md
@@ -15,25 +15,33 @@ The following instantiations are supported:
 * SHA2-256 (`HashLen` = 32)
 * SHA2-512 (`HashLen` = 64)
 
-### API Reference
-
-#### BLAKE2b
+### Available Implementations
 
 `````{tabs}
 ````{group-tab} 32
 ```C
 #include "Hacl_HKDF.h"
 ```
-
-```{doxygenfunction} Hacl_HKDF_extract_blake2b_32
-```
 ````
 
 ````{group-tab} 256
 ```C
 #include "Hacl_HKDF_Blake2b_256.h"
 ```
+````
+`````
+
+### API Reference
 
+#### BLAKE2b
+
+`````{tabs}
+````{group-tab} 32
+```{doxygenfunction} Hacl_HKDF_extract_blake2b_32
+```
+````
+
+````{group-tab} 256
 ```{doxygenfunction} Hacl_HKDF_Blake2b_256_extract_blake2b_256
 ```
 ````
diff --git a/docs/reference/hacl/mac/index.md b/docs/reference/hacl/mac/index.md
index 1f2e3ebe..41f51691 100644
--- a/docs/reference/hacl/mac/index.md
+++ b/docs/reference/hacl/mac/index.md
@@ -19,7 +19,7 @@ Keys must be chosen using a cryptographically strong pseudo-random generator and
 Note that the key can be of any length up to the specific block length of the used hash algorithm.
 This is also mentioned in the API reference below.
 
-## Implementations
+### Available Implementations
 
 `````{tabs}
 ````{group-tab} 32
@@ -51,8 +51,6 @@ Support for VEC256 is needed. Please see the [HACL Packages book].
 ````
 `````
 
---------------------------------------------------------------------------------
-
 #### BLAKE2s
 
 `````{tabs}
@@ -66,8 +64,6 @@ Support for VEC256 is needed. Please see the [HACL Packages book].
 ````
 `````
 
---------------------------------------------------------------------------------
-
 #### SHA-2
 
 ```{doxygenfunction} Hacl_HMAC_compute_sha2_256
@@ -79,8 +75,6 @@ Support for VEC256 is needed. Please see the [HACL Packages book].
 ```{doxygenfunction} Hacl_HMAC_compute_sha2_512
 ```
 
---------------------------------------------------------------------------------
-
 #### SHA-1
 
 ```{doxygenfunction} Hacl_HMAC_legacy_compute_sha1
diff --git a/docs/reference/hacl/randomness/index.md b/docs/reference/hacl/randomness/index.md
index a3e4f342..22d8fe46 100644
--- a/docs/reference/hacl/randomness/index.md
+++ b/docs/reference/hacl/randomness/index.md
@@ -4,12 +4,14 @@
 
 Deterministic Random Bit Generator (DRBG) (NIST, SP 800-90A).
 
-### API Reference
+### Available Implementations
 
 ```C
 #include "Hacl_HMAC_DRBG.h"
 ```
 
+### API Reference
+
 #### Variables
 
 ```{doxygenvariable} Hacl_HMAC_DRBG_reseed_interval
diff --git a/docs/reference/hacl/signature/ecdsa/k256.md b/docs/reference/hacl/signature/ecdsa/k256.md
index 680ad08d..ba917411 100644
--- a/docs/reference/hacl/signature/ecdsa/k256.md
+++ b/docs/reference/hacl/signature/ecdsa/k256.md
@@ -1,15 +1,26 @@
-<!-- Note: This module is already well-documented. Blocked by https://github.com/cryspen/hacl-star/issues/14 -->
-
 # K-256
 
 ECDSA over the secp256k1 curve.
 
-## API Reference
+## Available Implementations
 
 ```C
 #include "Hacl_K256_ECDSA.h"
 ```
 
+## API Reference
+
+<!--
+**Example**
+
+```{literalinclude} ../../../../tests/k256_ecdsa.cc
+:language: C
+:dedent:
+:start-after: "// START"
+:end-before: "// END"
+```
+-->
+
 ### Load and Store Keys
 
 ```{doxygenfunction} Hacl_K256_ECDSA_public_key_compressed_from_raw
@@ -72,15 +83,3 @@ TODO(API): No validate functions?
 ```{doxygenfunction} Hacl_K256_ECDSA_secp256k1_ecdsa_signature_normalize
 ```
 
-**Example**
-
-<!--
-TODO(Example):
-
-```{literalinclude} ../../../../tests/k256_ecdsa.cc
-:language: C
-:dedent:
-:start-after: "// START"
-:end-before: "// END"
-```
--->
diff --git a/docs/reference/hacl/signature/ecdsa/p256.md b/docs/reference/hacl/signature/ecdsa/p256.md
index 20f6dc99..0bfa63e1 100644
--- a/docs/reference/hacl/signature/ecdsa/p256.md
+++ b/docs/reference/hacl/signature/ecdsa/p256.md
@@ -1,13 +1,17 @@
-<!-- Note: This module is already well-documented in hacl-star. Blocked by https://github.com/cryspen/hacl-star/issues/14 -->
-
 # P-256
 
 ECDSA over the P-256 NIST curve.
 
-<!--
-TODO: Example
+## Available Implementations
+
+```C
+#include "Hacl_P256.h"
+```
 
-## Example
+## API Reference
+
+<!--
+**Example**
 
 ```{literalinclude} ../../../../tests/p256_ecdsa.cc
 :language: C
@@ -17,12 +21,6 @@ TODO: Example
 ```
 -->
 
-## API Reference
-
-```C
-#include "Hacl_P256.h"
-```
-
 ### Load and Store Keys
 
 ```{doxygenfunction} Hacl_P256_uncompressed_to_raw
diff --git a/docs/reference/hacl/signature/eddsa.md b/docs/reference/hacl/signature/eddsa.md
index ec0296b3..16de979e 100644
--- a/docs/reference/hacl/signature/eddsa.md
+++ b/docs/reference/hacl/signature/eddsa.md
@@ -11,12 +11,6 @@ Two APIs are exposed: A (simple) "One-Shot" API to sign/verify a single message
 
 ### One-Shot
 
-```{doxygenfunction} Hacl_Ed25519_sign
-```
-
-```{doxygenfunction} Hacl_Ed25519_verify
-```
-
 **Example**
 
 ```{literalinclude} ../../../../tests/ed25519.cc
@@ -26,14 +20,14 @@ Two APIs are exposed: A (simple) "One-Shot" API to sign/verify a single message
 :end-before: "// ANCHOR_END(example)"
 ```
 
-### Precomputed
-
-```{doxygenfunction} Hacl_Ed25519_expand_keys
+```{doxygenfunction} Hacl_Ed25519_sign
 ```
 
-```{doxygenfunction} Hacl_Ed25519_sign_expanded
+```{doxygenfunction} Hacl_Ed25519_verify
 ```
 
+### Precomputed
+
 **Example**
 
 ```{literalinclude} ../../../../tests/ed25519.cc
@@ -42,3 +36,10 @@ Two APIs are exposed: A (simple) "One-Shot" API to sign/verify a single message
 :start-after: "// ANCHOR(example precomputed)"
 :end-before: "// ANCHOR_END(example precomputed)"
 ```
+
+```{doxygenfunction} Hacl_Ed25519_expand_keys
+```
+
+```{doxygenfunction} Hacl_Ed25519_sign_expanded
+```
+
diff --git a/docs/reference/hacl/signature/rsapss.md b/docs/reference/hacl/signature/rsapss.md
index 46c2173f..2c4bfa23 100644
--- a/docs/reference/hacl/signature/rsapss.md
+++ b/docs/reference/hacl/signature/rsapss.md
@@ -2,10 +2,16 @@
 
 RSASSA-PSS as defined in [RFC 8017].
 
-<!--
-## Example
+## Available Implementations
+
+```C
+#include "Hacl_RSAPSS.h"
+```
+
+## API Reference
 
-TODO(Example):
+<!--
+**Example**
 
 ```{literalinclude} ../../../../tests/rsapss.cc
 :language: C
@@ -15,12 +21,6 @@ TODO(Example):
 ```
 -->
 
-## API Reference
-
-```C
-#include "Hacl_RSAPSS.h"
-```
-
 ```{doxygenfunction} Hacl_RSAPSS_new_rsapss_load_skey
 ```