This is a complete draft, but it still has lots of minor errors, and possibly some major ones. There are a number of small details missing from the specification, mostly concerning error conditions. Those details are apparently known only within Microsoft. I hope to talk to engineers there to learn these details and correct any inaccuracies in the specification.
The current specification provides a fairly simple model of the API, in which kernel calls and returns are atomic actions. The specification thus does not describe the details of how kernel calls are made. This seems to me to be the appropriate interface for application programmers (and for the implementers), who already understand how procedure calls are coded. I intend eventually to provide a lower-level specification that does model some of the details of kernel calls. I will do this by using an interface refinement that relates the higher-level and lower-level models of procedure calls, and is independent of the particular kernel calls being specified.
The specification is written in an "object oriented" style, which is discussed in the introduction.
The specification is: