diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2b1eb53..ab47af6 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -9,6 +9,13 @@ include(CTest)
 # Enable CTest
 enable_testing()
 
+# Enables LLVM builtin functions for memory operations. We do not check these for memory safety.
+# To check for memory safety, set this option to OFF. Then our wrappers will be used instead that
+# check for memory safety and call builtin functions directly.
+option(SEA_LLVM_MEM_BUILTINS "Use LLVM builtins memcpy/memmove without memory safety checks" OFF)
+
+option(SEA_ENABLE_CRAB "Enable Seahorn using Clam/Crab" OFF)
+
 if (CMAKE_SOURCE_DIR STREQUAL CMAKE_BINARY_DIR )
   message (FATAL_ERROR
     "In-source builds are not allowed. Please clean your source tree and try again.")
diff --git a/scripts/get_exper_brunch_stat.py b/scripts/get_exper_brunch_stat.py
new file mode 100644
index 0000000..bbb1e11
--- /dev/null
+++ b/scripts/get_exper_brunch_stat.py
@@ -0,0 +1,92 @@
+import re
+import csv
+import argparse
+from collections import defaultdict
+
+BRUNCH_DICT = {  # Dict stores csv columns to correspond name on BRUNCH STATS
+    "job_name": "Test: ",
+    "result": "Result",
+    "bmc.circ_sz": "bmc.circ_sz",
+    "bmc.dag_sz": "bmc.dag_sz",
+    "opsem.isderef.not.solve": "crab.isderef.not.solve",  # for crab
+    "opsem.isderef.solve": "crab.isderef.solve",  # for crab
+    "pp.isderef.not.solve": "crab.pp.isderef.not.solve",
+    "pp.isderef.solve": "crab.pp.isderef.solve", 
+    "bmc_time": "BMC",
+    "bmc_solve_time": "BMC.solve",
+    "opsem_crab_time": "opsem.crab",
+    "pp_crab_time": "seapp.crab",
+    "opsem_assert_time": "opsem.assert",
+    "opsem_simplify_time": "opsem.simplify",
+    "seahorn_total_time": "seahorn_total",
+    "object_domain_use_odi": "count.move_object",
+    "opsem_crab_solve_isderef": "opsem.time.crab.isderef"
+    # ADD additional coloumn and corresponded pattern on outputs here
+}
+
+
+def move_dict_items_to_lst(dt):
+    res = []
+    for key in BRUNCH_DICT:
+        if key == "job_name":
+            continue
+        if key not in dt:
+            res.append(0)
+        else:
+            res.append(dt[key])
+    return res
+
+
+def read_brunchstat_from_log(log_file_name, use_crab=False):
+    log_file = open(log_file_name, 'r')
+    line = log_file.readline()
+    data = defaultdict(list)
+    row_dict = {}
+    cur_test = None
+    while line:
+        # look for next test
+        new_test = re.search(BRUNCH_DICT["job_name"], line)
+        if new_test:
+            if cur_test:
+                data[cur_test] = move_dict_items_to_lst(row_dict)
+                row_dict.clear()
+            span = new_test.span()
+            test_name = line[span[1]:]
+            # remove _unsat_test
+            cur_test = test_name[:-12]
+        elif line.startswith("BRUNCH_STAT"):
+            stat = line.split()
+            # stat_name = " ".join(stat[1:-1])
+            stat_num = stat[-1]
+            for key in BRUNCH_DICT:
+                if stat[-2] == BRUNCH_DICT[key] or BRUNCH_DICT[key] in stat[-2]:
+                    row_dict[key] = stat_num
+        line = log_file.readline()
+    if cur_test:
+        data[cur_test] = move_dict_items_to_lst(row_dict)
+    log_file.close()
+    return data
+
+
+def write_brunchstat_into_csv(data, out_file):
+    print(out_file)
+    with open(out_file, 'w+', newline='') as csvfile:
+        writer = csv.writer(csvfile)
+        writer.writerow(list(BRUNCH_DICT.keys()))
+        for k, v in data.items():
+            writer.writerow([k, *v])
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(
+        description='in and out files')
+    parser.add_argument('logfile', type=str, help=".log file to read from")
+    parser.add_argument(
+        '--outfile',
+        '-o',
+        type=str,
+        default="brunch_stat.csv",
+        help="ouput csv filename")
+    args = parser.parse_args()
+    data = read_brunchstat_from_log(args.logfile)
+    write_brunchstat_into_csv(data, args.outfile)
diff --git a/scripts/get_exper_res.py b/scripts/get_exper_res.py
new file mode 100644
index 0000000..24cf1ce
--- /dev/null
+++ b/scripts/get_exper_res.py
@@ -0,0 +1,143 @@
+import xml.etree.ElementTree as ET
+import sys
+import os
+import csv
+import glob
+import subprocess
+import argparse
+from get_exper_brunch_stat import read_brunchstat_from_log, write_brunchstat_into_csv
+
+BUILDABSPATH = os.path.abspath('../build/')
+DATAABSPATH = os.path.abspath('../') + "/data"
+SEAHORN_ROOT = '../../build-seahorn-rgn'  # Put your seahorn root dir here
+FILE_DICT = {
+    "": "seahorn.csv",
+    "--vac": "seahorn(vac).csv",
+    "--horn-bmc-solver=smt-y2": "seahorn(smt-y2).csv",
+    "--cex": "seahorn(cex).csv",
+    "--cex --horn-bmc-solver=smt-y2": "seahorn(cex, smt-y2).csv",
+    "klee": "klee.csv"}
+
+
+def extra_to_filename(extra, suffix='.csv', prefix=''):
+    '''extra: --a=b --c=d to filename: a.b.c.d.csv'''
+    if (len(extra) == 0):
+        return f'base{suffix}'
+    parts = []
+    for flag in extra:
+        if flag.startswith('--'):
+            flag = flag[2:]
+        parts.extend(flag.split('='))
+    return f'{prefix}{"_".join(parts)}{suffix}'
+
+
+def make_build_path(extra, build_path='../build'):
+    build_path += extra_to_filename(extra, '', '_') if extra else '_base'
+    print(f'[Build Path] {build_path}')
+    if not os.path.exists(build_path):
+        os.mkdir(build_path)
+    global BUILDABSPATH
+    BUILDABSPATH = os.path.abspath(build_path)
+
+
+def get_output_level():
+    if args.debug:
+        output_level = sys.stdout
+    else:
+        output_level = subprocess.PIPE
+    return output_level
+
+
+def make_new_cmake_conf():
+    use_crab = "ON" if "--crab" in extra else "OFF"
+    return f'cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10\
+    -DCMAKE_CXX_COMPILER=clang++-10 -DSEA_ENABLE_CRAB={use_crab}\
+    -DSEAHORN_ROOT={SEAHORN_ROOT} -DTRUSTY_TARGET=x86_64 ../ -GNinja'
+
+
+def read_data_from_xml(res_data):
+    xml_file = glob.glob(
+        "{path}/**/Test.xml".format(path=BUILDABSPATH), recursive=True)[0]
+    tree = ET.parse(xml_file)
+    root = tree.getroot()
+    testlist = root.find('Testing')
+    for test in testlist.findall('Test'):
+        bench_name = test.find('Name').text
+        res = test.get('Status')
+        for name_measure_tag in test.find('Results').findall(
+                'NamedMeasurement'):
+            if name_measure_tag.attrib['name'] == 'Execution Time':
+                timing = name_measure_tag.find('Value').text
+        res_data.append([bench_name, timing, res])
+
+
+def write_data_into_csv(file_name, res_data):
+    with open(file_name, 'w+', newline='') as csvfile:
+        # create the csv writer object
+        csvwriter = csv.writer(csvfile)
+        csvwriter.writerow(["Name", "Timing", "Result"])
+        for row in res_data:
+            csvwriter.writerow(row)
+
+
+def collect_res_from_ctest(file_name):
+    res_data = []
+    read_data_from_xml(res_data)
+    write_data_into_csv(
+        "{dir}/{file}".format(dir="../data", file=file_name), res_data)
+    print("[Results] Please find result csv file at: ../data/%s" % file_name)
+
+
+def run_ctest_for_seahorn():
+    print("[SeaHorn] Start making SeaHorn results...")
+    set_env = ''
+    if extra and len(extra) > 0:
+        verify_flags = " ".join(extra)
+        print(f'Run SeaHorn with extra configs: {verify_flags} ')
+        set_env = f'env VERIFY_FLAGS=\"{verify_flags}\"'
+    cmake_conf = make_new_cmake_conf()
+    command_lst = ["rm -rf *", cmake_conf, "ninja",
+                   f'{set_env} ctest -j{os.cpu_count()} -D ExperimentalTest -R . --timeout {args.timeout}']
+    make_build_path(extra)
+    cddir = "cd " + BUILDABSPATH
+    for strcmd in command_lst:
+        cddir += " ; " + strcmd
+    if args.debug:
+        print(f'[Command] {cddir}')
+    process = subprocess.Popen(
+        '/bin/bash',
+        shell=True,
+        stdin=subprocess.PIPE,
+        stdout=get_output_level())
+    _ = process.communicate(cddir.encode())
+    collect_res_from_ctest(extra_to_filename(extra))
+    collect_stat_from_ctest_log(extra_to_filename(extra, suffix='.brunch.csv'),
+                                True if "--crab" in extra else False)
+
+
+def collect_stat_from_ctest_log(outfile, use_crab):
+    test_tmpdir = os.path.join(BUILDABSPATH, 'Testing', 'Temporary')
+    logfiles = [i for i in os.listdir(test_tmpdir)if os.path.isfile(
+        os.path.join(test_tmpdir, i)) and i.startswith("LastTest_")]
+    latest_log = logfiles[0]
+    print("collecting brunch stat from " + logfiles[0])
+    data = read_brunchstat_from_log(os.path.join(test_tmpdir, latest_log), use_crab)
+    outpath = os.path.join(DATAABSPATH, outfile)
+    write_brunchstat_into_csv(data, outpath)
+
+
+def main():
+    os.makedirs(DATAABSPATH, exist_ok=True)
+    os.makedirs(BUILDABSPATH, exist_ok=True)
+    run_ctest_for_seahorn()
+
+
+if __name__ == "__main__":
+    # Args for this script
+    parser = argparse.ArgumentParser(
+        description='Present flags to decide which tool will be tested.')
+    parser.add_argument('--debug', action='store_true', default=False)
+    parser.add_argument('--timeout', type=int, default=2000,
+                        help='Seconds before timeout for each test')
+    args, extra = parser.parse_known_args()
+    main()
diff --git a/scripts/get_loc_info.py b/scripts/get_loc_info.py
new file mode 100644
index 0000000..d82c557
--- /dev/null
+++ b/scripts/get_loc_info.py
@@ -0,0 +1,220 @@
+import sys
+import re
+import os
+import csv
+import glob
+import math
+import subprocess
+import argparse
+
+BUILDDIR = '../build/'
+BUILDABSPATH = os.path.abspath(BUILDDIR)
+DATAABSPATH = os.path.abspath('../') + "/data"
+HARNESS_PATH = f'{BUILDABSPATH}/seahorn/jobs'
+BENCHSUBDIRS = sorted(next(os.walk(f'{BUILDDIR}/seahorn/jobs'))[1])
+
+
+def get_regex_based_on_func_name(func_name):
+    name_1 = r"(define|declare).*@%s\(" % func_name
+    regexp1 = re.compile(name_1)
+    name_2 = fr'distinct !DISubprogram\((name: \"{func_name}\"|name: "call", linkageName: \"{func_name}\")'
+    regexp2 = re.compile(name_2)
+    return regexp1, regexp2
+
+
+def manipulate_input_data(data):
+    res_data = []
+    for x in data:
+        if x == '\n':
+            continue
+        else:
+            res_data.append(x)
+    return res_data
+
+
+def get_line_info(str_info):
+    line_loc_regexp = re.compile(r'!DILocation')
+    if not line_loc_regexp.search(str_info):
+        return -1
+    tmp_str = str_info.split("line: ")[1]
+    line = tmp_str.split(",")[0]
+    return line
+
+
+def comput_loc_for_a_func(data, srcidx, destidx):
+    max_line = -1
+    loc = 0
+    for idx in range(srcidx, destidx):
+        get_line_info
+        tmp = int(get_line_info(data[idx]))
+        if tmp > max_line:
+            max_line = tmp
+            loc += 1
+    return loc
+
+
+def current_func_loc(plain_data, name):
+    """
+     # This function compute line of code of a given function
+     # We gather line of info base on debug info
+     # Once we find any info by DILocation
+     # We overapproximate loc based on these line info
+     # Note that we may forget some lines but the loc we collected is consistent.
+     # @param plain_data stored data from .ll file.
+     # @param name the function name we used
+     # @return loc info if we find such function in debug info
+     # we treat loc as 1 if we hit some function does not contain body of function such as malloc func.
+    """
+    _, name_debug_regexp = get_regex_based_on_func_name(name)
+    next_function_debug_regexp = re.compile(r'distinct !DISubprogram')
+    for index, plain_d in enumerate(plain_data, start=1):
+        if name_debug_regexp.search(plain_d):
+            for indexp, plain_dp in enumerate(
+                    plain_data[index + 1:], start=index + 2):
+                if next_function_debug_regexp.search(plain_dp):
+                    loc = comput_loc_for_a_func(
+                        plain_data, index - 1, indexp - 1)
+                    return loc
+            return 1  # nd function treat as one line
+    raise Exception(f'the debug info of {name} must exists.')
+
+
+def get_next_func_call(data, name, index):
+    """
+     # This function compute a function call of a function based on given function name and index
+     # The function in our c file will have the following pattern:
+     #      call <blah blah> <func_name> <blah blah>
+     # Then it will find any function call within current function
+     # Finally we gather the function call info and return.
+     # @param data stored data from .ll file.
+     # @param name the function name we used
+     # @param index the index that we current pointed
+     # @return None if we hit the end of searching (when reach the pattern '}').
+     #          function name and debug function name and corresponded index on the data
+    """
+    func_call_regexp = re.compile(r'call.*@(?!llvm).*')
+    end_of_cur_func = re.compile(r'^}')
+    for index_next, line in enumerate(data[index:], start=index):
+        if end_of_cur_func.search(line):
+            return None, None, None  # end of searching...
+        if func_call_regexp.search(line):
+            func_name = line.split("@")[1].split("(")[0]
+            debug_name = func_name.split(
+                ".")[0] if "." in func_name else func_name
+            if func_name == name:
+                continue
+            return debug_name, func_name, index_next
+    return None, None, None
+
+
+def compute_loc_of_func(data, name, total_loc, func_dict):
+    """
+     # This function compute line of code of each function started by main
+     # We treat declare function as one line of code,
+     #      those function will be either simplified code or predefined code on seahorn
+     # The function recursively compute each called function on the harness
+     # Then it collect loc of current function and store it into total_loc
+     # @param data stored data from .ll file.
+     # @param name the function name we used
+     # @param total_loc the result of loc that we computed
+     # @param func_dict the dictionary to store function name we already computed
+     # @return nothing, use call by ref.
+    """
+    name_regexp, _ = get_regex_based_on_func_name(name)
+    for index, plain_d in enumerate(data, start=1):
+        if name_regexp.search(plain_d):
+            if 'declare' in plain_d:  # no definition, assume one line code
+                curr_loc = 0 if name in func_dict else 1
+                func_dict[name] = "done"
+            else:
+                while True:
+                    call_name, debug_name, index = get_next_func_call(
+                        data, name, index + 1)
+                    if not call_name and not debug_name:
+                        break
+                    if debug_name in func_dict:
+                        continue
+                    compute_loc_of_func(data, call_name, total_loc, func_dict)
+                    func_dict[debug_name] = "done"
+                curr_loc = current_func_loc(data, name)
+            if args.debug:
+                print(f'tot. {total_loc}, func <{name}> with loc: {curr_loc}')
+            total_loc[0] += curr_loc
+            break
+
+
+def read_output_from_file(file_name, bench_name):
+    try:
+        file = open(file_name, 'r')
+    except BaseException:
+        sys.exit("human readable bitcode (.ll) file does not exits. Exit!")
+    data = file.readlines()
+    if args.debug:
+        print(f'start compute loc for harness <{bench_name}>')
+    main_regexp, main_debug_regexp = get_regex_based_on_func_name('main')
+    res_data = ['', '']
+    # 1. Add harness name
+    res_data[0] = bench_name
+    loc = [0]
+    # 2. Add loc for each harness
+    func_dict = {}  # a dictionary to store any funcs we computed
+    compute_loc_of_func(data, 'main', loc, func_dict)
+    res_data[1] = loc[0]
+    if args.debug:
+        print(f'har. {bench_name} with loc comp. {res_data[1]}...')
+    file.close()
+    return res_data
+
+
+def run_llvmdis_for_harness(res_data):
+    """
+     # This function converts bitcode file into human readable files
+     # The command line is 'llvm-dis-10 <file_name>.bc'
+     # Then it will call function to compute loc based on .ll file
+     # @param res_data store all the infor we collected.
+     # @return nothing, use call by ref.
+    """
+    print("Start making LOC results ...")
+    for benchsubdir in BENCHSUBDIRS:
+        remain_path = f'{benchsubdir}/llvm-ir/{benchsubdir}.ir/{benchsubdir}.ir.bc'
+        file_name = f'{HARNESS_PATH}/{remain_path}'
+        command_lst = [f'llvm-dis-10 {file_name}']
+        cmd_llvmdis = ""
+        for strcmd in command_lst:
+            cmd_llvmdis += strcmd + " ; "
+        print(cmd_llvmdis)
+        process = subprocess.Popen(
+            '/bin/bash',
+            stdin=subprocess.PIPE,
+            stdout=subprocess.PIPE)
+        _ = process.communicate(cmd_llvmdis.encode())
+        file_name = file_name[:-2] + "ll"
+        # compute the loc
+        res_data.append(read_output_from_file(file_name, benchsubdir))
+
+
+def write_data_into_csv(file_name, res_data):
+    with open(file_name, 'w+', newline='') as csvfile:
+        # create the csv writer object
+        csvwriter = csv.writer(csvfile)
+        csvwriter.writerow(["Name", "LOC"])
+        for row in res_data:
+            # data = ', '.join(row)
+            csvwriter.writerow(row)
+
+
+def main():
+    os.makedirs(DATAABSPATH, exist_ok=True)
+    os.makedirs(BUILDABSPATH, exist_ok=True)
+    res_data = []
+    run_llvmdis_for_harness(res_data)
+    write_data_into_csv("../data/{file}".format(file='loc.csv'), res_data)
+
+
+if __name__ == "__main__":
+    # Args for this script
+    parser = argparse.ArgumentParser(
+        description='Present debug flag if using debug mode.')
+    parser.add_argument('--debug', action='store_true', default=False)
+    args = parser.parse_args()
+    main()
diff --git a/seahorn/CMakeLists.txt b/seahorn/CMakeLists.txt
index d1f6d61..4574f55 100644
--- a/seahorn/CMakeLists.txt
+++ b/seahorn/CMakeLists.txt
@@ -196,6 +196,9 @@ function(sea_attach_bc name)
   endif()
 
   target_compile_definitions(${SOURCE_EXE} PRIVATE __SEAHORN__)
+  if(SEA_ENABLE_CRAB)
+    target_compile_definitions(${SOURCE_EXE} PRIVATE __CRAB__)
+  endif()
   target_compile_definitions(${SOURCE_EXE} PRIVATE VACCHECK)
 
   # convert ${SOURCE_EXE} target to llvm
@@ -227,11 +230,17 @@ endfunction()
 
 function(sea_attach_bc_link name)
   sea_link_libraries(${name} sea_libc_trusty.ir)
+  if(SEA_ENABLE_CRAB)
+    sea_link_libraries(${name} crab_proofs.ir)
+  endif()
   sea_attach_bc(${name})
 endfunction()
 
 function(sea_attach_bc_cc_link name)
   sea_link_libraries(${name} sea_libc_trusty.ir)
+  if(SEA_ENABLE_CRAB)
+    sea_link_libraries(${name} crab_proofs.ir)
+  endif()
   sea_attach_bc_cc(${name})
 endfunction()
 
diff --git a/seahorn/sea_crab_base.yaml b/seahorn/sea_crab_base.yaml
new file mode 100644
index 0000000..14a7e9f
--- /dev/null
+++ b/seahorn/sea_crab_base.yaml
@@ -0,0 +1,20 @@
+verify_options:
+  horn-unify-assumes: false
+  horn-gsa: false
+# ignore control flow
+  horn-vcgen-only-dataflow: false
+# reduce by data dependence
+  horn-bmc-coi: false
+# Use crab solve sea.is_deref
+  horn-bmc-crab-dom: 'zones'
+  horn-bv2-crab-check-is-deref: ''
+# reduce used by object domain
+  # horn-bv2-crab-reduce: ''
+# Use crab infer allocation range
+  # horn-bv2-crab-rng: ''
+# Use crab solve sea.is_deref (preprocessing)
+  seapp-crab-dom: 'zones'
+  seapp-crab-lower-is-deref: true
+  # seapp-crab-stats: ''
+# Statistics
+  # horn-bv2-crab-stats: ''
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt
index f1b09a8..5e7fa75 100644
--- a/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt
+++ b/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt
@@ -1,10 +1,19 @@
 set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty)
+if(SEA_ENABLE_CRAB)
+add_library(
+  sea_libc_trusty
+  ${EXTERNAL}/ipc.c
+  crab_handle_table.c
+  crab_trusty_syscalls_impl.c
+)
+else()
 add_library(
   sea_libc_trusty
   ${EXTERNAL}/ipc.c
   sea_handle_table.c
   trusty_syscalls_impl.c
 )
+endif() 
 
 target_include_directories(sea_libc_trusty PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
 
diff --git a/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.c b/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.c
new file mode 100644
index 0000000..bdff54b
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.c
@@ -0,0 +1,417 @@
+/**
+   Implementation of table of handles to be used by IPC
+ */
+
+/** Global variables that keep current handle information */
+
+#include "sea_handle_table.h"
+#include <nondet.h>
+#include <seahorn/seahorn.h>
+
+#define NUM_PHANDLE 2
+#define NUM_CHANDLE 2
+
+
+struct handle {
+  handle_t id;
+  bool active;
+  void *cookie;
+
+  /* port only */
+  char path;
+  /* channel only */
+  uint32_t msg_id;
+  size_t msg_len;
+};
+
+/** Globals */
+// Define a global handle table for crab
+struct handle port_handle_1;
+struct handle port_handle_2;
+struct handle chan_handle_3;
+struct handle chan_handle_4;
+
+unsigned num_active_phandles = 0;
+unsigned num_active_chandles = 0;
+
+/**************************** Port operations *************************/
+/**
+  Init a port handle
+*/
+void init_port_handle(struct handle *ptr, handle_t id) {
+  ptr->id = id;
+  ptr->active = false;
+  ptr->cookie = NULL;
+  ptr->path = '\0';
+}
+
+/**
+   Returns the first port handle that is not active
+
+   Returns NULL if no port handle is available
+ */
+static struct handle *s_first_available_port_handle(bool secure) {
+  // search for a new port
+  struct handle *ptr = &port_handle_1;
+  if ((IS_SECURE_IPC_HANDLE(1) == secure) && !ptr->active) {
+    init_port_handle(ptr, 1);
+    return ptr;
+  }
+  ptr = &port_handle_2;
+  if ((IS_SECURE_IPC_HANDLE(2) == secure) && !ptr->active) {
+    init_port_handle(ptr, 2);
+    return ptr;
+  }
+  // if no port available
+  return NULL;
+}
+
+/**
+   Returns the first port handle that is not active
+   make it as active and set the path by the first character of path
+   FIXME: the implemantation of path is brittle, we only store / compare
+          the first character of path.
+
+   Returns INVALID_IPC_HANDLE if no port handle is available
+ */
+handle_t sea_ht_new_port(bool secure, const char *path) {
+  // search for a new port
+  struct handle *ptr = &port_handle_1;
+  if ((IS_SECURE_IPC_HANDLE(1) == secure) && !ptr->active) {
+    init_port_handle(ptr, 1);
+    num_active_phandles++;
+    ptr->active = true;
+    ptr->path = path[0];
+    return ptr->id;
+  }
+  ptr = &port_handle_2;
+  if ((IS_SECURE_IPC_HANDLE(2) == secure) && !ptr->active) {
+    init_port_handle(ptr, 2);
+    num_active_phandles++;
+    ptr->active = true;
+    ptr->path = path[0];
+    return ptr->id;
+  }
+  // if no port available
+  return INVALID_IPC_HANDLE;
+}
+
+handle_t sea_ht_match_port(const char *path) {
+  if (path) {
+    struct handle *ptr = &port_handle_1;
+    // NOTE: we only compare the first character
+    if (path[0] == ptr->path) {
+      return ptr->id;
+    }
+    ptr = &port_handle_2;
+    if (path[0] == ptr->path) {
+      return ptr->id;
+    }
+  }
+  return INVALID_IPC_HANDLE;
+}
+
+int sea_ht_free_port(handle_t handle) {
+  struct handle *ptr = &port_handle_1;
+  if (handle == ptr->id) {
+    ptr->active = false;
+    --num_active_phandles;
+    return NO_ERROR;
+  }
+  ptr = &port_handle_2;
+  if (handle == ptr->id) {
+    ptr->active = false;
+    --num_active_phandles;
+    return NO_ERROR;
+  }
+  return ERR_BAD_HANDLE;
+}
+
+/**
+   Non-deterministically chooses an active port handle
+
+   INVALID_IPC_HANDLE if no active handle is available
+ */
+handle_t sea_ht_choose_active_port_handle(void) {
+  handle_t handle = nd_handle();
+  assume(IS_PORT_IPC_HANDLE(handle));
+  struct handle *ptr = &port_handle_1;
+  if (handle == ptr->id && ptr->active) {
+    return handle;
+  }
+  ptr = &port_handle_2;
+  if (handle == ptr->id && ptr->active) {
+    return handle;
+  }
+  return INVALID_IPC_HANDLE;
+}
+
+bool sea_ht_is_active_port(handle_t handle) {
+  struct handle *ptr = &port_handle_1;
+  if (handle == ptr->id) {
+    return ptr->active;
+  }
+  ptr = &port_handle_2;
+  if (handle == ptr->id) {
+    return ptr->active;
+  }
+  return false;
+}
+
+int sea_ht_set_cookie_port(handle_t handle, void *cookie) {
+  struct handle *ptr = &port_handle_1;
+  if (handle == ptr->id) {
+    ptr->cookie = cookie;
+    return NO_ERROR;
+  }
+  ptr = &port_handle_2;
+  if (handle == ptr->id) {
+    ptr->cookie = cookie;
+    return NO_ERROR;
+  }
+  return ERR_BAD_HANDLE;
+}
+
+void *sea_ht_get_cookie_port(handle_t handle) {
+  struct handle *ptr = &port_handle_1;
+  if (handle == ptr->id) {
+    return ptr->cookie;
+  }
+  ptr = &port_handle_2;
+  if (handle == ptr->id) {
+    return ptr->cookie;
+  }
+  return NULL;
+}
+
+/**************************** Channel operations *************************/
+/**
+  Init a channel handle
+*/
+void init_channel_handle(struct handle *ptr, handle_t id) {
+  ptr->id = id;
+  ptr->active = false;
+  ptr->cookie = NULL;
+  ptr->path = '\0';
+  ptr->msg_id = 0;
+  ptr->msg_len = 0;
+}
+
+static struct handle *s_first_available_channel_handle(void) {
+  // search for a new channel
+  struct handle *ptr = &chan_handle_3;
+  if (!ptr->active) {
+    init_channel_handle(ptr, 3);
+    return ptr;
+  }
+  ptr = &chan_handle_4;
+  if (!ptr->active) {
+    init_channel_handle(ptr, 4);
+    return ptr;
+  }
+
+  // if no channel available
+  return NULL;
+}
+
+handle_t sea_ht_new_channel(handle_t port) {
+  // search for a new channel
+  struct handle *ptr = &chan_handle_3;
+  if (!ptr->active) {
+    init_channel_handle(ptr, 3);
+    num_active_chandles++;
+    ptr->active = true;
+    return ptr->id;
+    ;
+  }
+  ptr = &chan_handle_4;
+  if (!ptr->active) {
+    init_channel_handle(ptr, 4);
+    num_active_chandles++;
+    ptr->active = true;
+    return ptr->id;
+    ;
+  }
+  return INVALID_IPC_HANDLE;
+}
+
+int sea_ht_free_channel(handle_t handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (handle == ptr->id) {
+    ptr->active = false;
+    --num_active_chandles;
+    return NO_ERROR;
+  }
+  ptr = &chan_handle_4;
+  if (handle == ptr->id) {
+    ptr->active = false;
+    --num_active_chandles;
+    return NO_ERROR;
+  }
+  return ERR_BAD_HANDLE;
+}
+
+/**
+   Non-deterministically chooses an active channel handle
+
+   INVALID_IPC_HANDLE if no active handle is available
+ */
+handle_t sea_ht_choose_active_channel_handle(void) {
+  handle_t handle = nd_handle();
+  assume(IS_CHAN_IPC_HANDLE(handle));
+  struct handle *ptr = &chan_handle_3;
+  if (handle == ptr->id && ptr->active) {
+    return handle;
+  }
+  ptr = &chan_handle_4;
+  if (handle == ptr->id && ptr->active) {
+    return handle;
+  }
+  return INVALID_IPC_HANDLE;
+}
+
+int sea_ht_set_cookie_channel(handle_t handle, void *cookie) {
+  struct handle *ptr = &chan_handle_3;
+  if (handle == ptr->id) {
+    ptr->cookie = cookie;
+    return NO_ERROR;
+  }
+  ptr = &chan_handle_4;
+  if (handle == ptr->id) {
+    ptr->cookie = cookie;
+    return NO_ERROR;
+  }
+  return ERR_BAD_HANDLE;
+}
+
+void *sea_ht_get_cookie_channel(handle_t handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (handle == ptr->id) {
+    return ptr->cookie;
+  }
+  ptr = &chan_handle_4;
+  if (handle == ptr->id) {
+    return ptr->cookie;
+  }
+  return NULL;
+}
+
+bool sea_ht_has_msg(handle_t chan_handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_id > INVALID_IPC_MSG_ID;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_id > INVALID_IPC_MSG_ID;
+  }
+  return false;
+}
+
+uint32_t sea_ht_get_msg_id(handle_t chan_handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_id;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_id;
+  }
+  return INVALID_IPC_MSG_ID;
+}
+
+void sea_ht_set_msg_id(handle_t chan_handle, uint32_t id) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    ptr->msg_id = id;
+    return;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    ptr->msg_id = id;
+    return;
+  }
+}
+
+size_t sea_ht_get_msg_len(handle_t chan_handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_len;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    return ptr->msg_len;
+  }
+  // return 0 length if handle not found
+  return 0;
+}
+
+void sea_ht_set_msg_len(handle_t chan_handle, size_t len) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    ptr->msg_len = len;
+    return;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    ptr->msg_len = len;
+    return;
+  }
+}
+
+void sea_ht_new_nd_msg(handle_t chan_handle) {
+  struct handle *ptr = &chan_handle_3;
+  if (chan_handle == ptr->id) {
+    ptr->msg_id = nd_msg_id();
+    ptr->msg_len = nd_msg_len();
+    assume(ptr->msg_id > INVALID_IPC_MSG_ID);
+    return;
+  }
+  ptr = &chan_handle_4;
+  if (chan_handle == ptr->id) {
+    ptr->msg_id = nd_msg_id();
+    ptr->msg_len = nd_msg_len();
+    assume(ptr->msg_id > INVALID_IPC_MSG_ID);
+    return;
+  }
+}
+
+/*************************** Miscellaneous operations *************************/
+int sea_ht_set_cookie(handle_t handle, void *cookie) {
+  if (IS_PORT_IPC_HANDLE(handle)) {
+    return sea_ht_set_cookie_port(handle, cookie);
+  } else if (IS_CHAN_IPC_HANDLE(handle)) {
+    return sea_ht_set_cookie_channel(handle, cookie);
+  } else {
+    return ERR_BAD_HANDLE;
+  }
+}
+
+void *sea_ht_get_cookie(handle_t handle) {
+  if (IS_PORT_IPC_HANDLE(handle)) {
+    return sea_ht_get_cookie_port(handle);
+  } else if (IS_CHAN_IPC_HANDLE(handle)) {
+    return sea_ht_get_cookie_channel(handle);
+  } else {
+    return NULL;
+  }
+}
+
+int sea_ht_free(handle_t handle) {
+  if (IS_PORT_IPC_HANDLE(handle)) {
+    return sea_ht_free_port(handle);
+  } else if (IS_CHAN_IPC_HANDLE(handle)) {
+    return sea_ht_free_channel(handle);
+  } else {
+    return ERR_BAD_HANDLE;
+  }
+}
+
+handle_t sea_ht_choose_active_handle(void) {
+  handle_t handle = sea_ht_choose_active_port_handle();
+  if (handle != INVALID_IPC_HANDLE) {
+    return handle;
+  } else {
+    return sea_ht_choose_active_channel_handle();
+  }
+}
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.h b/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.h
new file mode 100644
index 0000000..0bde7ab
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/libc-trusty/crab_handle_table.h
@@ -0,0 +1,49 @@
+#ifndef _CRAB_HANDLE_TABLE_H_
+#define _CRAB_HANDLE_TABLE_H_
+
+#include <stdbool.h>
+#include <trusty_ipc.h>
+
+// TODO: increase number of handles as needed
+#define FISRT_PORT_HANDLE 1
+#define SECOND_PORT_HANDLE 2
+
+// TODO: increase number of channels as needed
+#define FISRT_CHAN_HANDLE 3
+#define SECOND_CHAN_HANDLE 4
+
+#define IS_PORT_IPC_HANDLE(h)                                                  \
+  (FISRT_PORT_HANDLE <= h && h <= SECOND_PORT_HANDLE)
+#define IS_CHAN_IPC_HANDLE(h)                                                  \
+  (FISRT_CHAN_HANDLE <= h && h <= SECOND_CHAN_HANDLE)
+#define IS_SECURE_IPC_HANDLE(h) ((h)&0x1)
+#define IS_NONSECURE_IPC_HANDLE(h) (!IS_SECURE_HANDLE(h))
+
+#define INVALID_IPC_MSG_ID 0
+#define MAX_IPC_MSG_NUM 10
+
+handle_t sea_ht_new_port(bool secure, const char *path);
+handle_t sea_ht_new_channel(handle_t port);
+
+handle_t sea_ht_choose_active_handle(void);
+
+bool sea_ht_is_active_port(handle_t handle);
+
+void *sea_ht_get_cookie_port(handle_t handle);
+void *sea_ht_get_cookie_channel(handle_t handle);
+void *sea_ht_get_cookie(handle_t handle);
+
+int sea_ht_set_cookie_port(handle_t handle, void *cookie);
+int sea_ht_set_cookie_channel(handle_t handle, void *cookie);
+int sea_ht_set_cookie(handle_t handle, void *cookie);
+int sea_ht_free(handle_t handle);
+
+bool sea_ht_has_msg(handle_t chan_handle);
+uint32_t sea_ht_get_msg_id(handle_t chan_handle);
+void sea_ht_set_msg_id(handle_t chan_handle, uint32_t id);
+size_t sea_ht_get_msg_len(handle_t chan_handle);
+void sea_ht_set_msg_len(handle_t chan_handle, size_t len);
+void sea_ht_new_nd_msg(handle_t chan_handle);
+
+handle_t sea_ht_match_port(const char *path);
+#endif
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/libc-trusty/crab_trusty_syscalls_impl.c b/seahorn/trusty/user/base/lib/libc-trusty/crab_trusty_syscalls_impl.c
new file mode 100644
index 0000000..e86d1d0
--- /dev/null
+++ b/seahorn/trusty/user/base/lib/libc-trusty/crab_trusty_syscalls_impl.c
@@ -0,0 +1,389 @@
+#include "sea_handle_table.h"
+#include "trusty_syscalls.h"
+
+#include <uapi/err.h> // trusty errors definitions
+#include <nondet.h>
+#include <seahorn/seahorn.h>
+
+/******************************** Server APIs *********************************/
+
+/* Documentation from trusty API:
+  port_create()
+Creates a named service port.
+
+[in] path: The string name of the port (as described above). This name should be unique across the system; attempts to create a duplicate will fail.
+[in] num_recv_bufs: The maximum number of buffers that a channel on this port '
+can pre-allocate to facilitate the exchange of data with the client. 
+Buffers are counted separately for data going in both directions, 
+so specifying 1 here would mean 1 send and 1 receive buffer are preallocated.
+[in] recv_buf_size: Maximum size of each individual buffer in the above buffer set. 
+This value is protocol-dependent and effectively limits maximum message size you can exchange with peer
+[in] flags: A combination of flags that specifies additional port behavior
+
+[retval]: Handle to the port created if non-negative or a specific error if negative
+*/
+handle_t _trusty_port_create(const char *path, uint32_t num_recv_bufs,
+                             uint32_t recv_buf_size, uint32_t flags) {
+  (void)path;
+
+  if (num_recv_bufs == 0 || recv_buf_size == 0) {
+    // error if no buffers or zero buf size
+    return ERR_INVALID_ARGS; 
+  }
+
+  if (!path) return ERR_BAD_PATH; // error if path not exists
+
+  // IPC_PORT_ALLOW_TA_CONNECT - allows a connection from other secure apps
+  // IPC_PORT_ALLOW_NS_CONNECT - allows a connection from the non-secure world
+  bool secure = (flags & IPC_PORT_ALLOW_NS_CONNECT) &&
+                !(flags & IPC_PORT_ALLOW_TA_CONNECT);
+  return sea_ht_new_port(secure, path);
+}
+
+/* Documentation from trusty API:
+  accept()
+Accepts an incoming connection and gets a handle to a channel.
+
+[in] handle_id: Handle representing the port to which a client has connected
+[out] peer_uuid: Pointer to a uuud_t structure to be filled with the UUID of 
+  the connecting client application. It will be set to all zeros if the 
+  connection originated from the non-secure world.
+
+[retval]: Handle to a channel (if non-negative) on which the server can exchange 
+  messages with the client (or an error code otherwise)
+*/
+handle_t _trusty_accept(handle_t port_handle, uuid_t *peer_uuid) {
+  (void)port_handle;
+  handle_t chan = sea_ht_new_channel(port_handle);
+  if (chan != INVALID_IPC_HANDLE) {
+    if ((port_handle & IPC_PORT_ALLOW_TA_CONNECT) == 0) {
+      // non-secure world
+      peer_uuid->time_low = 0;
+      peer_uuid->time_mid = 0;
+      peer_uuid->time_hi_and_version = 0;
+    }
+    else {
+      // define peer_uuid to a dummy value
+      peer_uuid->time_low = nd_time_low();
+      peer_uuid->time_mid = nd_time_mid();
+      peer_uuid->time_hi_and_version = nd_time_hi_n_ver();
+    }
+  }
+  return chan;
+}
+
+
+/******************************** Client APIs *********************************/
+/* Documentation from trusty API:
+  connect()
+Initiates a connection to a port specified by name.
+
+[in] path: Name of a port published by a Trusty application
+[in] flags: Specifies additional, optional behavior
+
+[retval]: Handle to a channel over which messages can be exchanged 
+with the server; error if negative
+*/
+handle_t _trusty_connect(const char *path, uint32_t flags) {
+  handle_t port_handle = sea_ht_match_port(path);
+  if (port_handle != INVALID_IPC_HANDLE) {
+    // if a port exists, create a new channel
+    return sea_ht_new_channel(port_handle);
+  }
+  return INVALID_IPC_HANDLE;
+}
+
+/******************************** Handle APIs *********************************/
+/* Documentation from trusty API:
+  set_cookie()
+Associates the caller-provided private data with a specified handle.
+
+[in] handle: Any handle returned by one of the API calls
+[in] cookie: Pointer to arbitrary user-space data in the Trusty application
+
+[retval]: NO_ERROR on success, error if negative
+*/
+int _trusty_set_cookie(handle_t handle, void *cookie) {
+  return sea_ht_set_cookie(handle, cookie);
+}
+
+/* Documentation from trusty API:
+  wait()
+Waits for an event to occur on a given handle for specified period of time.
+
+[in] handle_id: Any handle returned by one of the API calls
+[in] timeout_msecs: A timeout value in milliseconds; a value of -1 is an infinite timeout
+[out] event: A pointer to the structure representing an event that occurred on this handle
+
+[retval]: NO_ERROR if a valid event occurred within a timeout interval; 
+ERR_TIMED_OUT if a specified timeout elapsed but no event has occurred; 
+< 0 for other errors
+*/
+int _trusty_wait(handle_t handle, struct uevent *event,
+                 uint32_t timeout_msecs) {
+  (void)timeout_msecs;
+
+  int err = nd_trusty_ipc_err();
+  if (err < NO_ERROR)
+    return err;
+
+  if (handle == INVALID_IPC_HANDLE)
+    return handle;
+
+  event->handle = handle;
+  // NOTE: cookie may be null
+  event->cookie = sea_ht_get_cookie(handle);
+  event->event = nd_trusty_ipc_event();
+
+  if (IS_PORT_IPC_HANDLE(handle)) {
+    event->event = IPC_HANDLE_POLL_READY;
+  }
+
+  // Upon success (retval == NO_ERROR), fills a specified uevent_t structure 
+  // with information about the event that occurred.
+  if (IS_CHAN_IPC_HANDLE(handle)) {
+    if (event->event & IPC_HANDLE_POLL_MSG) {
+      // IPC_HANDLE_POLL_MSG indicates that 
+      // there is a pending message for this channel
+      if (sea_ht_get_msg_id(handle) == INVALID_IPC_MSG_ID) {
+        // pretend a message sent
+        sea_ht_new_nd_msg(handle);
+      }
+    }
+  }
+
+  return NO_ERROR;
+}
+
+/*
+  wait_any()
+Waits for an event to occur on any handles for specified period of time.
+
+[in] timeout_msecs: A timeout value in milliseconds; a value of -1 is an infinite timeout
+[out] event: A pointer to the structure representing an event that occurred on some handle
+
+[retval]: NO_ERROR if a valid event occurred within a timeout interval; 
+ERR_TIMED_OUT if a specified timeout elapsed but no event has occurred; 
+< 0 for other errors
+*/
+int _trusty_wait_any(uevent_t *ev, uint32_t timeout_msecs) {
+  (void)timeout_msecs;
+
+  int err = nd_trusty_ipc_err();
+  if (err < NO_ERROR)
+    return err;
+
+  handle_t h = sea_ht_choose_active_handle();
+  if (h == INVALID_IPC_HANDLE)
+    return h;
+
+  ev->handle = h;
+  // NOTE: cookie may be null
+  ev->cookie = sea_ht_get_cookie(h);
+  ev->event = nd_trusty_ipc_event();
+
+  if (IS_PORT_IPC_HANDLE(h)) {
+    ev->event = IPC_HANDLE_POLL_READY;
+  }
+
+  // Upon success (retval == NO_ERROR), fills a specified uevent_t structure 
+  // with information about the event that occurred.
+  if (IS_CHAN_IPC_HANDLE(h)) {
+    if (ev->event & IPC_HANDLE_POLL_MSG) {
+      // IPC_HANDLE_POLL_MSG indicates that 
+      // there is a pending message for this channel
+      if (sea_ht_get_msg_id(h) == INVALID_IPC_MSG_ID) {
+        // pretend a message sent
+        sea_ht_new_nd_msg(h);
+      }
+    }
+  }
+
+  return NO_ERROR;
+}
+/* Documentation from trusty API:
+  close()
+Destroys the resource associated with the specified handle and removes it from the handle table.
+
+[in] handle_id: Handle to destroy
+
+[retval]: 0 if success; a negative error otherwise
+*/
+
+int _trusty_close(handle_t handle) {
+  return sea_ht_free(handle);
+}
+
+handle_t _trusty_handle_set_create(void) { return INVALID_IPC_HANDLE; }
+
+int _trusty_handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent *evt) {
+  return ERR_GENERIC;
+}
+
+/******************************** Message APIs ********************************/
+/* Documentation from trusty API:
+  send_msg()
+Sends a message over a specified channel.
+
+[in] handle: Handle to the channel over which to send the message.
+[in] msg: Pointer to the ipc_msg_t structure describing the message.
+
+[retval]: Total number of bytes sent on success; a negative error otherwise.
+*/
+ssize_t _trusty_send_msg(handle_t handle, struct ipc_msg *msg) {
+  int err = nd_trusty_ipc_err();
+  if (err < NO_ERROR)
+    return err;
+  if (handle == INVALID_IPC_HANDLE || IS_PORT_IPC_HANDLE(handle))
+    return ERR_INVALID_ARGS;
+  if (!msg)
+    return ERR_FAULT;
+
+  sassert(0 <= msg->num_iov);
+  sassert(msg->num_iov <= MAX_IPC_MSG_NUM);
+
+  size_t sent_bytes = 0;
+  sea_ht_new_nd_msg(handle);
+  for (size_t i = 0; i < msg->num_iov; ++i) {
+    sent_bytes += msg->iov[i].iov_len;
+    sassert(sea_is_dereferenceable(msg->iov[i].iov_base, msg->iov[i].iov_len));
+  }
+  sea_ht_set_msg_len(handle, sent_bytes);
+  return sent_bytes;
+}
+
+/* Documentation from trusty API:
+  get_msg()
+Gets meta-information about the next message in an incoming message queue
+of a specified channel.
+
+[in] handle: Handle of the channel on which a new message must be retrieved.
+[out] msg_info: Message information structure described as follows:
+typedef struct ipc_msg_info {
+        size_t    len;
+        uint32_t  id;
+} ipc_msg_info_t;
+Each message is assigned a unique ID across the set of outstanding messages, 
+and the total length of each message is filled in. 
+If configured and allowed by the protocol, 
+there can be multiple outstanding (opened) messages at once for a particular channel.
+
+[retval]: NO_ERROR on success; a negative error otherwise
+*/
+int _trusty_get_msg(handle_t handle, struct ipc_msg_info *msg_info) {
+  if (handle == INVALID_IPC_HANDLE || IS_PORT_IPC_HANDLE(handle))
+    // get message on invalid handle
+    return ERR_INVALID_ARGS;
+  if (!msg_info) {
+    return ERR_GENERIC;
+  }
+  if (sea_ht_get_msg_id(handle) == INVALID_IPC_MSG_ID) {
+    return ERR_NO_MSG;
+  }
+  int err = nd_trusty_ipc_err();
+  if (err < NO_ERROR)
+    return err;
+
+  msg_info->id = sea_ht_get_msg_id(handle);
+  msg_info->len = sea_ht_get_msg_len(handle);
+
+  return msg_info->id != INVALID_IPC_MSG_ID ? NO_ERROR : INVALID_IPC_MSG_ID;
+}
+
+/* Documentation from trusty API:
+  read_msg()
+Reads the content of the message with the specified ID starting from the 
+specified offset.
+
+[in] handle: Handle of the channel from which to read the message.
+[in] msg_id: ID of the message to read.
+[in] offset: Offset into the message from which to start reading.
+[in] msg: Pointer to the ipc_msg_t structure describing a set of buffers into 
+which to store incoming message data.
+
+[retval]: Total number of bytes stored in the dst buffers on success; 
+a negative error otherwise.
+*/
+ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset,
+                         struct ipc_msg *msg) {
+  if (handle == INVALID_IPC_HANDLE || IS_PORT_IPC_HANDLE(handle))
+    // read message on invalid handle
+    return ERR_INVALID_ARGS;
+
+  if (sea_ht_get_msg_id(handle) != msg_id)
+    // read message on invalid msg id
+    return ERR_INVALID_ARGS;
+
+  if (!msg)
+    // read message on invalid msg
+    return ERR_FAULT;
+  
+  // if no msg on this channel
+  if (sea_ht_get_msg_id(handle) == INVALID_IPC_MSG_ID) {
+    return ERR_NO_MSG;
+  }
+
+  sassert(0 <= msg->num_iov);
+  sassert(msg->num_iov <= MAX_IPC_MSG_NUM);
+
+  size_t msg_len = sea_ht_get_msg_len(handle);
+  if (msg_len < 0)
+    // although this should not happened, just in case
+    return ERR_GENERIC;
+
+  if (offset > msg_len)
+    // read with invalid offset
+    return ERR_INVALID_ARGS;
+  sassert(offset <= msg_len);
+
+  msg_len -= offset;
+
+  size_t num_bytes_read = 0;
+  #pragma unroll MAX_IPC_MSG_NUM
+  for (size_t i = 0; i < msg->num_iov; ++i) {
+    if (msg_len < msg->iov[i].iov_len) {
+      sassert(sea_is_dereferenceable(msg->iov[i].iov_base, msg_len));
+      memhavoc(msg->iov[i].iov_base, msg_len);
+      num_bytes_read += msg_len;
+      return num_bytes_read;
+    }
+    sassert(sea_is_dereferenceable(msg->iov[i].iov_base,  msg->iov[i].iov_len));
+    memhavoc(msg->iov[i].iov_base, msg->iov[i].iov_len);
+    num_bytes_read += msg->iov[i].iov_len;
+    // avoid msg_len underflow
+    if (msg->iov[i].iov_len < msg_len) {
+      msg_len -= msg->iov[i].iov_len;
+    } else {
+      msg_len = 0;
+    }
+  }
+
+  return num_bytes_read;
+}
+
+/* Documentation from trusty API:
+  put_msg()
+Retires a message with a specified ID.
+
+[in] handle: Handle of the channel on which the message has arrived.
+[in] msg_id: ID of message being retired.
+
+[retval]: NO_ERROR on success; a negative error otherwise.
+*/
+int _trusty_put_msg(handle_t handle, uint32_t msg_id) {
+  int err = nd_trusty_ipc_err();
+  if (err < NO_ERROR)
+    return err;
+
+  if (handle == INVALID_IPC_HANDLE || IS_PORT_IPC_HANDLE(handle))
+    // read message on invalid handle
+    return ERR_INVALID_ARGS;
+
+  if (sea_ht_get_msg_id(handle) != msg_id)
+    // read message on invalid msg id
+    return ERR_INVALID_ARGS;
+
+  sea_ht_set_msg_id(handle, INVALID_IPC_MSG_ID);
+  sea_ht_set_msg_len(handle, 0);
+  return NO_ERROR;
+}
\ No newline at end of file
diff --git a/seahorn/trusty/user/base/lib/libc-trusty/sea_handle_table.h b/seahorn/trusty/user/base/lib/libc-trusty/sea_handle_table.h
index 203d134..e11ee35 100644
--- a/seahorn/trusty/user/base/lib/libc-trusty/sea_handle_table.h
+++ b/seahorn/trusty/user/base/lib/libc-trusty/sea_handle_table.h
@@ -4,6 +4,7 @@
 #include <stdbool.h>
 #include <trusty_ipc.h>
 
+#ifndef __CRAB__
 // TODO: increase number of handles as needed
 #define PORT_HANDLE_MIN 1
 #define PORT_HANDLE_MAX 2
@@ -45,4 +46,7 @@ void sea_ht_set_msg_len(handle_t chan_handle, size_t len);
 void sea_ht_new_nd_msg(handle_t chan_handle);
 
 handle_t sea_ht_math_port(const char *path);
+#else
+#include "crab_handle_table.h"
+#endif
 #endif
diff --git a/seahorn/trusty_common/include/nondet.h b/seahorn/trusty_common/include/nondet.h
index 8346722..4b35f94 100644
--- a/seahorn/trusty_common/include/nondet.h
+++ b/seahorn/trusty_common/include/nondet.h
@@ -1,5 +1,6 @@
+#include <stdbool.h>
+#include <stddef.h>
 #include <stdint.h>
-#include <stdlib.h>
 #include <trusty_ipc.h> // -> ipc structs
 
 #include <uapi/err.h> // trusty errors definitions
@@ -11,15 +12,22 @@ extern "C" {
 long nd_long(void);
 uint16_t nd_short(void);
 int32_t nd_int(void);
+bool nd_bool(void);
 uint8_t nd_char(void);
 uint32_t nd_unsigned(void);
+uint32_t nd_uint32_t(void);
+uint64_t nd_uint64_t(void);
 void* nd_ptr(void);
+size_t nd_size_t(void);
+ssize_t nd_ssize_t(void);
+unsigned int nd_uint(void);
 
 /**
  * for functions with return pattern:
  * NO_ERROR on success; a negative error otherwise
  **/
 int nd_trusty_errs(void);
+handle_t nd_handle(void);
 
 /* port_create */
 handle_t nd_port_handle(void);
@@ -63,6 +71,13 @@ int nd_wait_ret(void);
 int nd_store_mem_size(void);
 size_t nd_get_alloc_size(void);
 
+/* ipc */
+uint32_t nd_trusty_ipc_event(void);
+int nd_trusty_ipc_err(void);
+
+/* */
+void memhavoc(void *ptr, size_t size);
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/seahorn/trusty_common/lib/CMakeLists.txt b/seahorn/trusty_common/lib/CMakeLists.txt
index 678928a..63a677b 100644
--- a/seahorn/trusty_common/lib/CMakeLists.txt
+++ b/seahorn/trusty_common/lib/CMakeLists.txt
@@ -9,3 +9,10 @@ if(SEA_ALLOCATOR_CAN_FAIL)
   target_compile_definitions(sea_common_proofs PRIVATE SEA_ALLOCATOR_CAN_FAIL)
 endif()
 sea_attach_bc(sea_common_proofs)
+
+
+# crab proof helpers
+if(SEA_ENABLE_CRAB)
+  add_library(crab_proofs nd_clam.c)
+  sea_attach_bc(crab_proofs)
+endif()
\ No newline at end of file
diff --git a/seahorn/trusty_common/lib/nd_clam.c b/seahorn/trusty_common/lib/nd_clam.c
new file mode 100644
index 0000000..ef7a971
--- /dev/null
+++ b/seahorn/trusty_common/lib/nd_clam.c
@@ -0,0 +1,113 @@
+#include <math.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include <seahorn/seahorn.h>
+#include "nondet.h"
+
+#define NONDET_FN_ATTR __declspec(noalias)
+
+extern NONDET_FN_ATTR int nd_int(void);
+extern NONDET_FN_ATTR int64_t nd_int64_t(void);
+extern NONDET_FN_ATTR int8_t  nd_int8_t(void);
+extern NONDET_FN_ATTR int16_t nd_int16_t(void);
+extern NONDET_FN_ATTR int32_t nd_int32_t(void);
+extern handle_t NONDET_FN_ATTR nd_handle(void);
+
+extern uint32_t NONDET_FN_ATTR nd_time_low(void);
+extern uint16_t NONDET_FN_ATTR nd_time_mid(void);
+extern uint16_t NONDET_FN_ATTR nd_time_hi_n_ver(void);
+
+extern int NONDET_FN_ATTR nd_trusty_ipc_err(void);
+extern uint32_t nd_trusty_ipc_event(void);
+
+bool nd_malloc_is_fail(void) {
+  // make assumption for crab
+  // malloc always safe
+  return false;
+}
+
+size_t nd_size_t(void) {
+  int64_t res = nd_int64_t();
+  __VERIFIER_assume(res >= 0);
+  return (size_t)res;
+}  
+
+uint8_t nd_uint8_t(void) {
+  int8_t res = nd_int8_t();
+  __VERIFIER_assume(res >= 0);
+  return (uint8_t)res;  
+}
+
+uint16_t nd_uint16_t(void) {
+  int16_t res = nd_int16_t();
+  __VERIFIER_assume(res >= 0);
+  return (uint16_t)res;  
+}
+
+uint32_t nd_uint32_t(void) {
+  int32_t res = nd_int32_t();
+  __VERIFIER_assume(res >= 0);
+  return (uint32_t)res;  
+}
+
+uint64_t nd_uint64_t(void) {
+  int64_t res = nd_int64_t();
+  __VERIFIER_assume(res >= 0);
+  return (uint64_t)res;    
+}
+
+handle_t nd_handle(void) {
+  return nd_int32_t();
+}
+
+uint32_t nd_time_low(void) {
+  return nd_uint32_t();
+}
+
+uint16_t nd_time_mid(void) {
+  return nd_uint16_t();
+}
+
+uint16_t nd_time_hi_n_ver(void) {
+  return nd_uint16_t();
+}
+
+int nd_trusty_ipc_err(void) {
+  return nd_int();
+}
+
+uint32_t nd_trusty_ipc_event(void) {
+  uint32_t res = nd_uint32_t();
+  __VERIFIER_assume(res >= 0 && res <= IPC_HANDLE_POLL_SEND_UNBLOCKED);
+  return res;
+}
+
+int nd_store_mem_size(void) {
+  return nd_int();
+}
+
+size_t nd_msg_len(void) {
+  return nd_size_t();
+}
+
+uint32_t nd_msg_id(void) {
+  return nd_uint32_t();
+}
+
+uint16_t nd_short(void) {
+  return nd_uint16_t();
+}
+
+ssize_t nd_ssize_t(void) {
+  int64_t res = nd_int64_t();
+  return (ssize_t)res;
+}
+
+unsigned int nd_uint(void) {
+  return nd_uint32_t();
+}
\ No newline at end of file
diff --git a/seahorn/trusty_common/lib/nondet.c b/seahorn/trusty_common/lib/nondet.c
index 021d7b6..17bfc80 100644
--- a/seahorn/trusty_common/lib/nondet.c
+++ b/seahorn/trusty_common/lib/nondet.c
@@ -24,3 +24,5 @@ int nd_set_cookie_ret(void) { return nd_trusty_errs(); }
 int nd_close_ret(void) { return nd_trusty_errs(); }
 
 int nd_wait_ret(void) { return nd_trusty_errs(); }
+
+void RAND_bytes(void *ptr, size_t size) { memhavoc(ptr, size); }
\ No newline at end of file
diff --git a/verify.py.in b/verify.py.in
index 4bd3196..75e60a4 100755
--- a/verify.py.in
+++ b/verify.py.in
@@ -57,6 +57,8 @@ def main(argv):
                               help='Counterexample mode')
             argp.add_argument('--vac', action='store_true', default=False,
                               help='Vacuity mode')
+            argp.add_argument('--crab', action='store_true', default=False,
+                              help='Using crab')
             argp.add_argument('input_file', nargs=1)
             argp.add_argument('--dry-run', dest='dry_run',
                               action='store_true', default=False,
@@ -109,6 +111,12 @@ def main(argv):
                                           'sea.vac.yaml')
                 cmd.extend(['-y', vac_config])
 
+            # crab config
+            if args.crab:
+                crab_config = os.path.join(script_dir, 'seahorn', 
+                                          'sea.crab.yaml')
+                cmd.extend(['-y', crab_config])
+
             # job specific config
             job_config = os.path.abspath(os.path.join(file_dir, '..', '..',
                                                       'sea.yaml'))