Are invariants on the kernel data structures documented?
 

I want to program a kind of a security module as an example, and I want later to prove that my code is enforcing the invariants on a specific data structure (e.g., those in /include/linux/list.h). But I'm not sure what the invariants are. So, are the invariants documented anywhere?

nope

I don't get it. Just because the word 'assert' does not appear you are concluding that the invariants are not documented?

How and where would you document them?

Well, I'm quite certain that other word that 'assert' can be used. It is indeed a good point but, realying only on this, the conclusion that no invariants are documented is a bit far fetched in my opinion. Anyway thanks for the info, I appreciate it.