diff --git a/fstar/api/MLS.fst b/fstar/api/MLS.fst
index 42c9a0e..06633a6 100644
--- a/fstar/api/MLS.fst
+++ b/fstar/api/MLS.fst
@@ -213,7 +213,8 @@ let process_commit state wire_format message message_auth =
   let? (state, encryption_secret) = (
     match message_content.path with
     | None -> (
-      let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.commit state.treekem_state None None provisional_group_context new_group_context in
+      let? pend = MLS.TreeKEM.API.prepare_process_add_only_commit state.treekem_state in
+      let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.finalize_process_commit pend None new_group_context in
       return ({ state with treekem_state;}, encryption_secret)
     )
     | Some path ->
@@ -236,11 +237,13 @@ let process_commit state wire_format message message_auth =
           assume(MLS.NetworkBinder.Properties.path_filtering_ok state.treekem_state.tree_state.tree treekem_path);
           assume(~(List.Tot.memP state.leaf_index (List.Tot.map snd added_leaves)));
           let open MLS.TreeKEM.API in
-          MLS.TreeKEM.API.commit state.treekem_state (Some {
+          let? pend = MLS.TreeKEM.API.prepare_process_full_commit state.treekem_state {
             commit_leaf_ind = _;
             path = treekem_path;
             excluded_leaves = (List.Tot.map snd added_leaves);
-          }) None provisional_group_context new_group_context
+            provisional_group_context;
+          } in
+          MLS.TreeKEM.API.finalize_process_commit pend None new_group_context
         )
       in
       return ({ state with treesync_state; treekem_state;}, encryption_secret)
@@ -446,7 +449,7 @@ let generate_welcome_message st ratchet_tree new_group_context confirmation_tag
 
 type generate_update_path_result (leaf_index:nat) = {
   update_path: update_path_nt bytes;
-  pending_commit: MLS.TreeKEM.API.pending_commit_2 bytes leaf_index;
+  pending_commit: MLS.TreeKEM.API.pending_create_commit_2 bytes leaf_index;
   provisional_group_context: group_context_nt bytes;
   ratchet_tree: ratchet_tree_nt bytes tkt;
   path_secrets: list (key_package_nt bytes tkt & bytes);
diff --git a/fstar/treekem/code/MLS.TreeKEM.API.fst b/fstar/treekem/code/MLS.TreeKEM.API.fst
index 8d71251..8616be7 100644
--- a/fstar/treekem/code/MLS.TreeKEM.API.fst
+++ b/fstar/treekem/code/MLS.TreeKEM.API.fst
@@ -84,23 +84,43 @@ type full_commit_args (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:
   commit_leaf_ind: commit_leaf_ind:MLS.TreeKEM.API.Tree.Types.treekem_index st{commit_leaf_ind <> leaf_ind};
   path: path:pathkem bytes st.levels 0 commit_leaf_ind{path_filtering_ok st.tree path};
   excluded_leaves: excluded_leaves:list nat{~(List.Tot.memP leaf_ind excluded_leaves)};
+  provisional_group_context: group_context_nt bytes;
 }
 
-val commit:
+type pending_process_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
+  next_tree_state: treekem_tree_state bytes leaf_ind;
+  opt_commit_secret: option bytes;
+}
+
+val prepare_process_full_commit:
+  #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
+  st:treekem_state bytes leaf_ind -> full_commit_args st.tree_state ->
+  result (pending_process_commit st)
+let prepare_process_full_commit #bytes #cb #leaf_ind st args =
+  let? (next_tree_state, commit_secret) = T.commit st.tree_state args.path args.excluded_leaves args.provisional_group_context in
+  return ({
+    next_tree_state;
+    opt_commit_secret = Some commit_secret;
+  })
+
+val prepare_process_add_only_commit:
   #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
-  st:treekem_state bytes leaf_ind -> option (full_commit_args st.tree_state) -> option bytes -> group_context_nt bytes -> group_context_nt bytes ->
+  st:treekem_state bytes leaf_ind ->
+  result (pending_process_commit st)
+let prepare_process_add_only_commit #bytes #cb #leaf_ind st =
+  return ({
+    next_tree_state = st.tree_state;
+    opt_commit_secret = None;
+  })
+
+val finalize_process_commit:
+  #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat -> #st:treekem_state bytes leaf_ind ->
+  pending_process_commit st -> option bytes -> group_context_nt bytes ->
   result (treekem_state bytes leaf_ind & bytes)
-let commit #bytes #cb #leaf_ind st opt_full_commit_args opt_psk provisional_group_context new_group_context =
-  let? (tree_state, opt_commit_secret) =
-    match opt_full_commit_args with
-    | None -> return (st.tree_state, None)
-    | Some args ->
-      let? (new_tree_state, commit_secret) = T.commit st.tree_state args.path args.excluded_leaves provisional_group_context in
-      return (new_tree_state, Some commit_secret)
-  in
-  let? (keyschedule_state, encryption_secret, _) = KS.commit st.keyschedule_state opt_commit_secret opt_psk new_group_context in
+let finalize_process_commit #bytes #cb #leaf_ind #st pend opt_psk new_group_context =
+  let? (keyschedule_state, encryption_secret, _) = KS.commit st.keyschedule_state pend.opt_commit_secret opt_psk new_group_context in
   return ({
-    tree_state;
+    tree_state = pend.next_tree_state;
     keyschedule_state;
   }, encryption_secret)
 
@@ -112,7 +132,7 @@ val prepare_create_commit_entropy_lengths:
 let prepare_create_commit_entropy_lengths bytes #cb =
   T.prepare_create_commit_entropy_lengths bytes
 
-type pending_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
+type pending_create_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
   pend: MLS.TreeKEM.API.Tree.pending_commit st.tree_state;
 }
 
@@ -120,7 +140,7 @@ val prepare_create_commit:
   #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
   st:treekem_state bytes leaf_ind ->
   randomness bytes (prepare_create_commit_entropy_lengths bytes) ->
-  result (pending_commit st & pre_pathkem bytes st.tree_state.levels 0 leaf_ind)
+  result (pending_create_commit st & pre_pathkem bytes st.tree_state.levels 0 leaf_ind)
 let prepare_create_commit #bytes #cb #leaf_ind st rand =
   let? (pend, path) = T.prepare_create_commit st.tree_state rand in
   return ({pend}, path)
@@ -132,7 +152,7 @@ val continue_create_commit_entropy_lengths:
 let continue_create_commit_entropy_lengths #bytes #cb #leaf_ind st added_leaves =
   T.finalize_create_commit_entropy_lengths st.tree_state added_leaves
 
-type pending_commit_2 (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind:nat) = {
+type pending_create_commit_2 (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind:nat) = {
   new_state: treekem_state bytes leaf_ind;
   commit_secret: bytes;
 }
@@ -145,10 +165,10 @@ type continue_create_commit_result (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_
 val continue_create_commit:
   #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
   #st:treekem_state bytes leaf_ind ->
-  pending_commit st ->
+  pending_create_commit st ->
   added_leaves:list nat -> group_context_nt bytes ->
   randomness bytes (continue_create_commit_entropy_lengths st added_leaves) ->
-  result (pending_commit_2 bytes leaf_ind & continue_create_commit_result st)
+  result (pending_create_commit_2 bytes leaf_ind & continue_create_commit_result st)
 let continue_create_commit #bytes #cb #leaf_ind #st pending added_leaves provisional_group_context randomness =
   let? tree_commit_result = T.finalize_create_commit #bytes pending.pend added_leaves provisional_group_context randomness in
   let new_state = { st with
@@ -172,7 +192,7 @@ type create_commit_result (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind: nat) =
 
 val finalize_create_commit:
   #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
-  pending_commit_2 bytes leaf_ind  ->
+  pending_create_commit_2 bytes leaf_ind  ->
   group_context_nt bytes -> option bytes ->
   result (create_commit_result bytes leaf_ind)
 let finalize_create_commit #bytes #cb #leaf_ind pending new_group_context opt_psk =