diff --git a/CMakeLists.txt b/CMakeLists.txt
index 810b01d..dc6342f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -67,6 +67,7 @@ include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/hwkey/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/keymaster/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/rng/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/storage/include)
+include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/tipc/include)
 include_directories(${TRUSTY_ROOT}/trusty/kernel/include/uapi/)
 include_directories(${TRUSTY_ROOT}/trusty/kernel/lib/ubsan/include)
 include_directories(${TRUSTY_ROOT}/system/gatekeeper/include/)
diff --git a/seahorn/trusty/CMakeLists.txt b/seahorn/trusty/CMakeLists.txt
index e692b86..2bb96bd 100644
--- a/seahorn/trusty/CMakeLists.txt
+++ b/seahorn/trusty/CMakeLists.txt
@@ -1 +1,2 @@
 add_subdirectory(user/base/lib/libc-trusty)
+add_subdirectory(user/base/lib/tipc)
diff --git a/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt
new file mode 100644
index 0000000..f4e987a
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt
@@ -0,0 +1,14 @@
+include_directories(include)
+
+set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/tipc)
+add_library(
+  sea_trusty_tipc
+  ${EXTERNAL}/tipc.c
+  trusty_ipc_impl.c
+)
+
+target_include_directories(sea_trusty_tipc PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
+
+sea_attach_bc(sea_trusty_tipc)
+
+add_subdirectory(proof)
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h
new file mode 100644
index 0000000..0e0bcef
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h
@@ -0,0 +1,20 @@
+#pragma once
+
+#include <trusty_ipc.h>
+
+
+
+ssize_t send_msg(handle_t handle, struct ipc_msg *msg);
+
+typedef struct State{
+    int msg_send_called;
+    int msg_recv_called;
+} state;
+
+state g_state;
+
+void state_init(void);
+void msg_sent(void);
+void msg_received(void);
+void state_reset(void);
+int get_msg_sent_times(void);
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt
new file mode 100644
index 0000000..545dccf
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_subdirectory(tipc_connect)
+add_subdirectory(tipc_send1)
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt
new file mode 100644
index 0000000..86c63e0
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt
@@ -0,0 +1,5 @@
+add_executable(tipc_connect_pf main.c)
+sea_link_libraries(tipc_connect_pf sea_trusty_tipc.ir)
+
+sea_attach_bc(tipc_connect_pf)
+sea_add_unsat_test(tipc_connect_pf)
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c
new file mode 100644
index 0000000..c113264
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c
@@ -0,0 +1,13 @@
+#include <seahorn/seahorn.h>
+#include <lib/tipc/tipc.h>
+#include <trusty_ipc.h>
+
+int main(void) {
+  int rc;
+  handle_t h = INVALID_IPC_HANDLE;
+  char path[64];
+
+  /* Make tipc_connect fail and check if handle is unchanged */
+  rc = tipc_connect(&h, NULL);
+  sassert(rc <= 0);
+} 
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt
new file mode 100644
index 0000000..1db4fdb
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt
@@ -0,0 +1,5 @@
+add_executable(tipc_send1_pf main.c)
+sea_link_libraries(tipc_send1_pf sea_trusty_tipc.ir)
+
+sea_attach_bc(tipc_send1_pf)
+sea_add_unsat_test(tipc_send1_pf)
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c
new file mode 100644
index 0000000..d7cd3e2
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c
@@ -0,0 +1,36 @@
+#include <seahorn/seahorn.h>
+#include <lib/tipc/tipc.h>
+#include <trusty_ipc.h>
+#include <sea_tipc_helper.h>
+
+extern handle_t nd_handle(void);
+extern int nd_size_t(void);
+extern void *sea_malloc_havoc(size_t sz);
+
+/** Test harness for tpic_send1 */
+int main(void) {
+
+    
+    /* assumptions */
+    state_init();
+    handle_t handle = nd_handle();
+
+    size_t buf_len = nd_size_t();
+    assume(buf_len > 0);
+
+    void *buf = sea_malloc_havoc(buf_len);
+    
+//   sea_tracking_on();
+//   sea_reset_modified((char *)buf);
+
+   /* send single buf message  */
+   int rc = tipc_send1(handle, buf, buf_len);
+
+ //  sassert(!sea_is_modified((char *)buf));
+
+   /* testing the message is only sent once */
+   int msg_sent = get_msg_sent_times();
+   sassert(msg_sent == 1);
+   state_reset();
+   return 0;
+}
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c
new file mode 100644
index 0000000..7078c1b
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c
@@ -0,0 +1,93 @@
+/**
+ * Stubbed version of trusty IPC
+ **/
+
+//#include <trusty_ipc.h>
+#include <nondet.h>
+#include <seahorn/seahorn.h>
+#include <sea_tipc_helper.h>
+
+extern int nd_size_t(void);
+extern int msg_send_called;
+
+void state_init(void)
+{
+    g_state.msg_recv_called = 0;
+    g_state.msg_send_called = 0;
+}
+void msg_sent(void){
+    g_state.msg_send_called += 1;
+}
+void msg_received(void){
+    g_state.msg_recv_called += 1;
+}
+void state_reset(void){
+    g_state.msg_recv_called = 0;
+    g_state.msg_send_called = 0;
+}
+
+int get_msg_sent_times(void){
+    return g_state.msg_send_called;
+}
+
+handle_t port_create(const char* path,
+                     uint32_t num_recv_bufs,
+                     uint32_t recv_buf_size,
+                     uint32_t flags) {
+    return nd_port_handle();
+}
+
+handle_t connect(const char* path, uint32_t flags) {
+    handle_t rc =  nd_chan_handle();
+    assume(rc <= 0);
+    return rc;
+}
+
+handle_t accept(handle_t handle, struct uuid* peer_uuid) {
+    return nd_chan_handle();
+}
+
+int close(handle_t handle) {
+    return nd_int();
+}
+
+int set_cookie(handle_t handle, void* cookie) {
+    return nd_int();
+}
+
+handle_t handle_set_create(void) {
+    return nd_chan_handle();
+}
+
+int handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent* evt) {
+    return nd_int();
+}
+
+int wait(handle_t handle, struct uevent* event, uint32_t timeout_msecs) {
+    return nd_int();
+}
+
+int wait_any(struct uevent* event, uint32_t timeout_msecs) {
+    return nd_int();
+}
+
+int get_msg(handle_t handle, struct ipc_msg_info* msg_info) {
+    return nd_int();
+}
+
+ssize_t read_msg(handle_t handle,
+                 uint32_t msg_id,
+                 uint32_t offset,
+                 struct ipc_msg* msg) {
+    return nd_int();
+}
+
+int put_msg(handle_t handle, uint32_t msg_id) {
+    return nd_int();
+}
+
+ssize_t send_msg(handle_t handle, struct ipc_msg* msg) {
+    msg_sent();
+    return nd_size_t();
+}
+