"A tapasztalat pedig azt mutatja, hogy még a formálisan ellenőrzött seL4 mikrokernelben is vannak függvénymutatókat érintő kasztolási hibák."
Az eleg erdekes, ugyanis az sel4-ban egyaltalan function pointer hivasok sincsenek. Function pointert egyedul ott hasznalnak, ahol ez a hw miatt kell (pl. IDT), meg a debug kodban, de az nem resze a proofnak.