L4.sec implementation and formal verification