The Verified Software Toolchain (VST) gives us a powerful tool for proving correctness of C programs. With the recent addition of mechanisms for external state, we can even reason about the behavior of programs that communicate with the outside world, for instance via network sockets or console I/O. But the implementations of these communication functions cannot be verified with VST: they involve the state of the operating system and interactions with device drivers, and break the usual single-program, single-memory abstraction of user-level programs. In this talk, we will present work on connecting VST proofs to system call implementations in CertiKOS, the verified operating system, which uses a different approach to verifying (kernel-level) C code. Such a connection must bridge the gap between VST’s step-indexed, ownership-annotated model of memory and CertiKOS’s more concrete representation, as well as establishing a common language for talking about communication events across user programs and the OS.