The various Keykos kernels shared most of the invariants but the prose describing these invariants is most complete for the 370 assembler version where they are referred to as ‘assertions’.
There is a brief introduction to these ideas here in the kernel logic manual and the more compete list is found later here.
The detailed invariants are phrased so as to make the code easy to design but also understand the meaning and perhaps motive for the invariant.
Much jargon here is from the IBM System/370 Principles of Operation.