diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 1959884..5140419 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -11,7 +11,7 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  CREUSOT_VERSION: v0.10.0+why3find-dep
+  CREUSOT_VERSION: v0.11.0
 
 jobs:
   rust:
diff --git a/.github/workflows/nightly.yaml b/.github/workflows/nightly.yaml
index ceafc47..e94d432 100644
--- a/.github/workflows/nightly.yaml
+++ b/.github/workflows/nightly.yaml
@@ -50,4 +50,4 @@ jobs:
           echo -e '[patch.crates-io]\ncreusot-std = { path = "../creusot/creusot-std" }' > .cargo/config.toml
 
       - name: Run Creusot
-        run: cargo creusot prove -- -Fsolutions
+        run: cargo creusot -- -Fsolutions
diff --git a/Cargo.lock b/Cargo.lock
index deb2909..6ac632d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -10,9 +10,7 @@ checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8"
 
 [[package]]
 name = "creusot-std"
-version = "0.10.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6496cade7c540734f2db0e40c7a0be29c2fe3a056efdc67b3b7770b56baca4ff"
+version = "0.11.0"
 dependencies = [
  "creusot-std-proc",
  "num-rational",
@@ -20,9 +18,7 @@ dependencies = [
 
 [[package]]
 name = "creusot-std-proc"
-version = "0.10.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a617b331f778b6e199b66057395f63b9d977573e4ca0856a33b8d169d0f0a640"
+version = "0.11.0"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/Cargo.toml b/Cargo.toml
index ac0c90d..b6d02df 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2024"
 
 [dependencies]
-creusot-std = { version = "0.10.0", features = ["sc-drf"] }
+creusot-std = { version = "0.11.0-dev", features = ["sc-drf"] }
 
 [features]
 solutions = []
diff --git a/src/ex3_parallel_add.rs b/src/ex3_parallel_add.rs
index 6ce8dfd..09d0b68 100644
--- a/src/ex3_parallel_add.rs
+++ b/src/ex3_parallel_add.rs
@@ -6,7 +6,6 @@
 #[allow(unused)] // TODO: Remove this
 use creusot_std::{
     ghost::{
-        Committer,
         invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace},
         perm::Perm,
         resource::{Authority, Fragment},
@@ -16,8 +15,8 @@ use creusot_std::{
 };
 
 use std::sync::atomic::AtomicI32;
-// TODO: Replace with the creusot_std version of AtomicI32
-// use creusot_std::std::sync::AtomicI32;
+// TODO: Replace with the creusot_std version of AtomicI32 (you will also need the committer ☺)
+// use creusot_std::sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer};
 
 use std::thread;
 // TODO: Replace with the creusot_std version of thread
diff --git a/src/solutions/ex3_parallel_add.rs b/src/solutions/ex3_parallel_add.rs
index 411da29..293330e 100644
--- a/src/solutions/ex3_parallel_add.rs
+++ b/src/solutions/ex3_parallel_add.rs
@@ -1,14 +1,15 @@
-use creusot_std::std::sync::atomic_sc::AtomicI32;
 use creusot_std::{
     ghost::{
-        Committer,
-        invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace},
+        invariant::{AtomicInvariantSC, Protocol, Tokens, declare_namespace},
         perm::Perm,
         resource::{Authority, Fragment},
     },
     logic::{Id, ra::excl::Excl},
     prelude::*,
-    std::thread::{self, JoinHandleExt},
+    std::{
+        sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer},
+        thread::{self, JoinHandleExt},
+    },
 };
 
 declare_namespace! { PARALLEL_ADD }
@@ -48,7 +49,7 @@ pub fn parallel_add() -> i32 {
     };
 
     // Initialize our invariant
-    let inv = AtomicInvariant::new(
+    let inv = AtomicInvariantSC::new(
         ghost!(ParallelAddAtomicInv {
             own: own.into_inner(),
             auth1: auth1.into_inner(),
@@ -59,7 +60,7 @@ pub fn parallel_add() -> i32 {
     );
 
     thread::scope(|s| {
-        // We use move closure to make sure that they do not contain borrows of `Ghost<_>`, since
+        // We use move closures to make sure that they do not contain borrows of `Ghost<_>`, since
         // such a borrow would unnecesary consume space in these closures. So, we create the borrows
         // here.
         let mut frag1: Ghost<&mut _> = frag1.borrow_mut();
@@ -70,10 +71,11 @@ pub fn parallel_add() -> i32 {
         let t1 = s.spawn(move |tokens: Ghost<Tokens>| {
             atomic.fetch_add(
                 2,
-                ghost! { |c: &mut Committer<AtomicI32>| {
+                ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| {
                     inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| {
                         inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true)))));
-                        c.shoot(&mut inv.own);
+                        c.shoot_load(&inv.own);
+                        c.shoot_store(&mut inv.own);
                     })
                 }},
             );
@@ -82,10 +84,11 @@ pub fn parallel_add() -> i32 {
         let t2 = s.spawn(move |tokens: Ghost<Tokens>| {
             atomic.fetch_add(
                 2,
-                ghost! { |c: &mut Committer<AtomicI32>| {
+                ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| {
                     inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| {
                         inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true)))));
-                        c.shoot(&mut inv.own);
+                        c.shoot_load(&inv.own);
+                        c.shoot_store(&mut inv.own);
                     })
                 }},
             );