1. seL4 exists. I haven't seen much more formal and rigorous than it. Efforts have ported the Linux kernel and RTOS-things to it.

2. Add syscall(s) to POSIX, which encourages *nix adoption, with an API like the following:

- Drop capabilities for thread/process except allow list.

- Test if current thread/process has all listed capabilities.

- List should be able to represent capabilities and their attributes, much like a single unveil() OpenBSD call, maybe as an array of/pointer to struct.

- (Program crashes if syscall capability is missing.)