The main difference is the verification/design method. seL4 does the abstract machine in Haskell, model in HOL, and final code in C. Both Haskell and C are shown equivalent. It took a ton of work. They also have to use these two tools for expressing all kinds of solutions they're not ideal for.

CertiKOS is using a DSL approach if it's same as paper I'm remembering. They design languages or proving techniques ideal to the type of thing they're working on: memory management, I/O, etc. They prove each individual component as easily as they can. Then they have some way of modeling the system as a whole and/or integrating those. Too early to judge but they seem more productive than L4 project was due to tooling benefits.

I searched the conference paper for "sel4" and this result seems relevant to your question:

  A comparison of the performance of seL4 and mC2 is
  not straightforward since the verified mC2 kernel
  runs on a multicore x86 platform, while the verified
  seL4 kernel runs on ARMv6 and ARMv7 hardware and
  only supports single-core