From reading this:
Is the Haskell source code available?
Which “existing L4 specifications” do you recommend?
If the Haskell is the manual, where do I get the manual?
What manual gives the precise syntax for doing the memory VSpace calls in some (cross) supported language?
What is the content of the message delivered to the “thread’s page fault handler”?
In This paper:
The top-most layer beneath the capDL and security in the picture is the abstract specification: an operational level contains enough detail to specify the outer interface of the kernel, for example, how system-call arguments are encoded in binary form, and it describes in abstract logical terms the effect of each system call or what happens when an interrupt of virtual memory fault occurs.
It does not describe in detail now these effects are implemented in the kernel.
Has the “abstract specification” been published?