For example, the 2 UML diagrams that you linked look fairly different depending on whether you’re on single-core or multi-core.
Yes, and a diagram can be easily used to highlight a) the critical chain of events for a successful communication, b) which links in this chain are relying on scheduling details c) which links are relying on sequential scheduling. And it is this very distinction (whether an successful communication can take place, for example in the face of single-core/multi-core), which (implicit) assumptions on the scheduling have to be met for it to succeed, and (optionally) what step would make a failed communication observable that I'd wish to have more (and more visual!) documentation on. I know that this can be derived by hand by any engineer who understands the principles of Microkit + seL4, but that is an error prone process.