Arithmetic overflows and exceptions: humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4.
Er, 2038? You'll get a nice overflow at that point on a 32-bit machine.
L4 isn't UNIX. It doesn't even have a POSIX userland, necessarily, and certainly wasn't designed with 70s hardware limitations in mind.
<speculation>
The L4::Pistachio kernel provides direct access to high-resolution hardware timing interrupts, though the secure variant may restrict some timer access in order to prevent covert timing channels between threads in different security contexts.
</speculation>
Er, 2038? You'll get a nice overflow at that point on a 32-bit machine.