In recent years, deductive code verification has improved to a degree that makes it feasible for realworld programs. In the VerisoftXT subproject Avionics, the goal is to apply formal methods to a commercial embedded OS. In particular, the goal is to use deductive techniques to verify functional correctness of the PikeOS microkernel. For verification, we use tools like VCC (the Verifying C Compiler) developed by Microsoft Research, which is a batch-mode verification tool. First experiences with this new tool are described in this paper.