Currently, a service that needs to receive many notifications has a problem. The only scalable way to do so is to use an endpoint, but it is a bad idea for to make an IPC call to an untrusted endpoint, so this only works if the service is trusted.
I came up with the idea of notification queues, but Curtis Millar came up with a better suggestion: allow notifications to be bound to endpoints, rather than threads. Any number of notifications could be bound to an endpoint, so this scales to arbitrarily many notification objects. The only limit is available memory.
Sadly, I won’t be able to implement this in the near term, and even if I could, I have zero experience with Isabelle, so I wouldn’t be able to help with the verification changes. That said, I do believe that this is a good idea and would be willing to write an RFC for this.