One document for each system: what it is, how a query travels through it step by step, what it costs, how it fails, what must always hold and what is still open. Every claim points at a file and line in the code.