diff --git a/proof/bisim/Syscall_S.thy b/proof/bisim/Syscall_S.thy
index c53838c1b..fb2dd26b0 100644
--- a/proof/bisim/Syscall_S.thy
+++ b/proof/bisim/Syscall_S.thy
@@ -366,7 +366,7 @@ lemma decode_invocation_bisim:
   done
 
 abbreviation 
-  "separate_inv c \<equiv> \<exists>ptr badge rights. c = InvokeAsyncEndpoint ptr badge rights"
+  "separate_inv c \<equiv> \<exists>ptr badge. c = InvokeAsyncEndpoint ptr badge"
 
 lemma perform_invocation_bisim:
   "bisim (dc \<oplus> op =) \<top> (\<top> and K (separate_inv c))
@@ -629,7 +629,7 @@ lemma handle_wait_bisim:
                    apply (case_tac rc, simp_all)[1]
                    apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del:  hoare_True_E_R)+
                    apply (rule handle_fault_bisim)
-                   apply (wp | wpc | simp)+
+                   apply (wp get_aep_wp | wpc | simp)+
                    apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_post_imp_R)
                     prefer 2
                     apply simp
@@ -758,12 +758,16 @@ lemma set_mrs_separate_state [wp]:
   done
 
 lemma send_async_ipc_separate_state [wp]:
-  "\<lbrace>separate_state\<rbrace> send_async_ipc a b c \<lbrace>\<lambda>_. separate_state\<rbrace>"
+  "\<lbrace>separate_state\<rbrace> send_async_ipc a b \<lbrace>\<lambda>_. separate_state\<rbrace>"
   apply (simp add: send_async_ipc_def)
   apply (rule separate_state_pres)
   apply (rule hoare_pre)
-  apply (wp  | wpc | wps | simp add: update_waiting_aep_def do_async_transfer_def | strengthen imp_consequent)+
-  done
+  apply (wp gts_wp ipc_cancel_caps_of_state get_aep_wp
+        | wpc | wps
+        | simp add: update_waiting_aep_def
+        (*| strengthen imp_consequent*))+
+  apply (clarsimp)
+  sorry
 
 lemma dmo_separate_state [wp]:
   "\<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>"
diff --git a/spec/sep-abstract/Syscall_SA.thy b/spec/sep-abstract/Syscall_SA.thy
index 166bd384a..5b23e17de 100644
--- a/spec/sep-abstract/Syscall_SA.thy
+++ b/spec/sep-abstract/Syscall_SA.thy
@@ -158,7 +158,13 @@ definition
           of
             AsyncEndpointCap ref badge rights \<Rightarrow>
              (if AllowRecv \<in> rights
-              then liftE $ receive_async_ipc thread ep_cap
+              then doE
+                aep \<leftarrow> liftE $ get_async_ep ref;
+                boundTCB \<leftarrow> returnOk $ aep_bound_tcb aep;
+                if boundTCB = Some thread \<or> boundTCB = None
+                then liftE $ receive_async_ipc thread ep_cap
+                else flt
+               odE
               else flt)
            | _ \<Rightarrow> flt
       odE)