I would add Jochen Liedtke (unfortunately he passed away already more than 20 years ago) as inventor of the L4 microkernel.
Several research groups continued work on L4 after Liedtke's death (Hermann Härtig in Dresden, Gernot Heiser in Sydney, a bit of research at Frank Bellosa's group in Karlsruhe and more industrial research on L4 for embedded/RT systems by Robert Kaiser, later a professor in Wiesbaden), but I would still argue that Liedtke's original work was the most influential, though all the formal verification work in Sydney also had significant impact - but that was only enabled by the simplicity of the underlying microkernel concepts and implementations.
Several research groups continued work on L4 after Liedtke's death (Hermann Härtig in Dresden, Gernot Heiser in Sydney, a bit of research at Frank Bellosa's group in Karlsruhe and more industrial research on L4 for embedded/RT systems by Robert Kaiser, later a professor in Wiesbaden), but I would still argue that Liedtke's original work was the most influential, though all the formal verification work in Sydney also had significant impact - but that was only enabled by the simplicity of the underlying microkernel concepts and implementations.