Formalising the L4 microkernel API