And if a user _couldn't_ ptrace the processes they invoked? Congratulations, you've just made malware authors extremely happy.

Unix does have a decently strong, capability-based permission model. On the one hand, you have file descriptors which are literally anonymous resources to ad hoc system objects. Capsicum only required small tweaks to the Unix API to round it out.

On the other hand you have UIDs, GIDs, along with SUID and SGID bits on executables. A good example of how this can be used is BSD Auth, the BSD answer to PAM. Unlike PAM, which heavily relies on root permissions--typically by the authenticator itself--in BSD Auth authentication methods are implemented by binaries under /usr/libexec/auth/, most of which either have the SUID or (more typically) SGID bit set so the module runs with the necessary permissions to access the credential database without giving those permissions to the process initiating the authentication. Whether you use SUID or SGID depends on whether you want to restrict authentication; if so you limit execute permissions by GID and use SUID to switch roles, otherwise better to just use SGID.

BSD Auth shows the power of the Unix UID.GID model, but it's woefully underutilized. Which hints at a larger problem.
Our software sucks because we're all bad programmers. We keep rehashing things without understanding and making use of the tools at our disposal, and of course even when we use the correct architectures our software is buggy.

To my mind seL4 and, to a lesser extent Genode, isn't really about permission models. It's about being able to separate correctly written programs from broken programs. Until you can _absolutely_ trust the core software, obsessing over models and architectures is pointless. The reason Administrator and root permissions are so commonly used, and why privilege separation not more commonly applied, is because software is so buggy and broken that if you took away the ability for people (directly, or indirectly through another layer of software) to introspect/supplement/hack _privileged_ software, people would flock elsewhere because of the usability nightmare. I mean, this is how we ended up with VMs and containers, which are at _best_ a totally lateral move in terms of architectural and practical security.

seL4 and formal verification is about breaking that cycle so we can begin laying down a layer of trusted software upon which we can consistently and meaningfully make use of better security models. The capability models employed by seL4 are principally directed toward that end, not toward the end of making writing secure software easier for your typical C++ or Node.js developer. The capability and ACL models best suited for those developers will look and operate differently, and in all likelihood look very much more like the Unix-based models for various reasons--path dependency, practicality, and the fact that they're quite capable, especially if made more consistent (see, e.g. Capsicum wrt capabilities, Plan 9 wrt to namespace visibility, both of which are heavily based on file descriptors and the Unix UID/GID model). From a usability standpoint the key hurdle is figuring out the best semantics for the capability _broker_. L4 doesn't really address the broker problem directly; Unix and Plan 9 and various other systems do, which is simultaneously the source of their convenience and flaws.