Think I'm starting to understand this. My current understanding of a syscall is operations like read(), write() or mkdir() are implemented in the kernel. So they are executed at a higher execution level (e.g., Ring 0 in x64, EL1 in ARM64) and each have their own syscall numbers. Most user applications don't directly invoke them, but rather use a libc wrapper with the same syscall name. In seL4, this idea is a bit different. The kernel itself handles send+receive and yield (and also their variations) syscalls inside the kernel at a higher execution level. Object methods are implemented using those syscalls inside libsel4. Which executes at a lower execution level (e.g., Ring 4, EL0). Here I am, again, a little bit confused. Sorry. When I looked at the source and did some debugging I see that, as an example, UntypedRetype is implemented in libsel4 (sel4_client.h) Like you, and others, said it is implemented using send+receive system calls. So, everything is good so far. But, what about their syscall numbers you have mentioned that have been vectored for efficiency? I was not able to find them in the source (both after and before system call stub generation). I looked inside syscall.h after syscall_header_gen.py. I'm sure I'm missing something or my understanding of what a syscall needs more work. Thanks for the previous answers. It motivated me to debug an application (a tutorial) and see how parts of libsel4 is actually implemented. -T