They do but it's a little different. (P)NaCL still allows memory safety and data verification bugs that don't compromise the integrity of the sandbox. sel4 goes a lot further by verifying that the total behavior of the application matches the machine readable formal specification. So (P)NaCL probably would have allowed the bug in question to get into production, whereas it would have been caught as a build error by sel4.
