diff --git a/extract_to_fstar.py b/extract_to_fstar.py
index a8f5f6553..a5d1a146d 100755
--- a/extract_to_fstar.py
+++ b/extract_to_fstar.py
@@ -6,7 +6,7 @@
 import sys
 
 
-def shell(command, expect=0, cwd=None, format_filter_string=False):
+def shell(command, expect=0, cwd=None):
     subprocess_stdout = subprocess.DEVNULL
 
     print("Command: ", end="")
@@ -101,7 +101,6 @@ def shell(command, expect=0, cwd=None, format_filter_string=False):
             "fstar",
         ],
         cwd=options.crate_path,
-        format_filter_string=True,
     )
 elif options.kyber_reference:
     shell(
@@ -114,7 +113,6 @@ def shell(command, expect=0, cwd=None, format_filter_string=False):
             "fstar",
         ],
         cwd=".",
-        format_filter_string=True,
     )
 else:
     shell(["cargo", "hax", "into", "fstar"], cwd=options.crate_path)
diff --git a/specs/kyber/Cargo.toml b/specs/kyber/Cargo.toml
index c2b2a78d0..c03b0e028 100644
--- a/specs/kyber/Cargo.toml
+++ b/specs/kyber/Cargo.toml
@@ -8,14 +8,9 @@ libcrux = { version = "=0.0.2-pre.1", path = "../../" }
 hacspec-lib = { version = "0.0.1", path = "../hacspec-lib" }
 
 [dev-dependencies]
-criterion = "0.5.1"
 hex = { version = "0.4.3", features = ["serde"] }
 pqcrypto-kyber = { version = "0.7.6", default-features = false }
 proptest = "1.2.0"
 rand = "0.8.5"
 serde = { version = "1.0.171", features = ["derive"] }
 serde_json = "1.0.102"
-
-[[bench]]
-name = "kem"
-harness = false
diff --git a/specs/kyber/benches/kem.rs b/specs/kyber/benches/kem.rs
deleted file mode 100644
index 2697a4234..000000000
--- a/specs/kyber/benches/kem.rs
+++ /dev/null
@@ -1,122 +0,0 @@
-use criterion::{criterion_group, criterion_main, BatchSize, Criterion};
-
-use pqcrypto_kyber::kyber768;
-
-use rand;
-
-pub fn randombytes<const N: usize>() -> [u8; N] {
-    use rand::rngs::OsRng;
-    use rand::RngCore;
-
-    let mut bytes = [0u8; N];
-    OsRng.fill_bytes(&mut bytes);
-    bytes
-}
-
-pub fn comparisons_key_generation(c: &mut Criterion) {
-    let mut group = c.benchmark_group("Kyber768 Key Generation");
-
-    group.bench_function("libcrux specification", |b| {
-        b.iter_batched(
-            || {
-                let seed = randombytes::<{ hacspec_kyber::KYBER768_KEY_GENERATION_SEED_SIZE }>();
-                seed
-            },
-            |seed| {
-                let _key_pair = hacspec_kyber::generate_keypair(seed).unwrap();
-            },
-            BatchSize::SmallInput,
-        )
-    });
-
-    group.bench_function("pqclean reference implementation", |b| {
-        b.iter(|| {
-            let (_public_key, _secret_key) = kyber768::keypair();
-        })
-    });
-}
-
-pub fn comparisons_encapsulation(c: &mut Criterion) {
-    let mut group = c.benchmark_group("Kyber768 Encapsulation");
-
-    group.bench_function("libcrux specification", |b| {
-        b.iter_batched(
-            || {
-                let keygen_seed =
-                    randombytes::<{ hacspec_kyber::KYBER768_KEY_GENERATION_SEED_SIZE }>();
-                let key_pair = hacspec_kyber::generate_keypair(keygen_seed).unwrap();
-
-                let encaps_seed = randombytes::<{ hacspec_kyber::KYBER768_SHARED_SECRET_SIZE }>();
-
-                (key_pair.pk().clone(), encaps_seed)
-            },
-            |(public_key, encaps_seed)| {
-                let (_ciphertext, _shared_secret) =
-                    hacspec_kyber::encapsulate(public_key, encaps_seed).unwrap();
-            },
-            BatchSize::SmallInput,
-        )
-    });
-
-    group.bench_function("pqclean reference implementation", |b| {
-        b.iter_batched(
-            || {
-                let (public_key, _secret_key) = kyber768::keypair();
-
-                public_key
-            },
-            |public_key| {
-                let (_shared_secret, _ciphertext) = kyber768::encapsulate(&public_key);
-            },
-            BatchSize::SmallInput,
-        )
-    });
-}
-
-pub fn comparisons_decapsulation(c: &mut Criterion) {
-    let mut group = c.benchmark_group("Kyber768 Decapsulation");
-
-    group.bench_function("libcrux specification", |b| {
-        b.iter_batched(
-            || {
-                let keygen_seed =
-                    randombytes::<{ hacspec_kyber::KYBER768_KEY_GENERATION_SEED_SIZE }>();
-                let key_pair = hacspec_kyber::generate_keypair(keygen_seed).unwrap();
-
-                let encaps_seed = randombytes::<{ hacspec_kyber::KYBER768_SHARED_SECRET_SIZE }>();
-                let (ciphertext, _shared_secret) =
-                    hacspec_kyber::encapsulate(key_pair.pk().clone(), encaps_seed).unwrap();
-
-                (key_pair.sk().clone(), ciphertext)
-            },
-            |(secret_key, ciphertext)| {
-                let _shared_secret = hacspec_kyber::decapsulate(ciphertext, secret_key);
-            },
-            BatchSize::SmallInput,
-        )
-    });
-
-    group.bench_function("pqclean reference implementation", |b| {
-        b.iter_batched(
-            || {
-                let (public_key, secret_key) = kyber768::keypair();
-                let (_shared_secret, ciphertext) = kyber768::encapsulate(&public_key);
-
-                (ciphertext, secret_key)
-            },
-            |(ciphertext, secret_key)| {
-                let _shared_secret = kyber768::decapsulate(&ciphertext, &secret_key);
-            },
-            BatchSize::SmallInput,
-        )
-    });
-}
-
-pub fn comparisons(c: &mut Criterion) {
-    comparisons_key_generation(c);
-    comparisons_encapsulation(c);
-    comparisons_decapsulation(c);
-}
-
-criterion_group!(benches, comparisons);
-criterion_main!(benches);
diff --git a/specs/kyber/src/sampling.rs b/specs/kyber/src/sampling.rs
index b4519a4fd..fbfaa7389 100644
--- a/specs/kyber/src/sampling.rs
+++ b/specs/kyber/src/sampling.rs
@@ -232,6 +232,7 @@ mod tests {
 
     proptest! {
         #[test]
+        #[ignore = "see https://github.com/cryspen/libcrux/issues/112"]
         fn uniform_sampler_mean_and_variance(randomness in vec(any::<u8>(), REJECTION_SAMPLING_ATTEMPTS * parameters::REJECTION_SAMPLING_SEED_SIZE)) {
             let mut sampled_ring_element = KyberPolynomialRingElement::ZERO;
 
@@ -277,6 +278,7 @@ mod tests {
         }
 
         #[test]
+        #[ignore = "see https://github.com/cryspen/libcrux/issues/112"]
         fn binomial_sampler_mean_and_variance(
             randomness in vec(any::<u8>(), 2 * 2 * 64)
             )