Multi-agent systems

Audit: did the system follow its own rules?

Check the process from the record \(G\) alone (steps and record, arrival times), without judging any proof: a run that follows its rules can still prove something false.

(process invariant)

A property \(P(G)\) that every run following the skill's rules satisfies, whatever the problem. If \(P(G)\) fails, a rule was broken, and the check names the steps.

check_invariants.py tests I1–I6 on any run record (tree.json, older runs data.json).

Process invariants, checked on the worked example (106 agent steps, root steps R-1…R-4).
invariant	definition	result
I1 independence	\(u\to v,\ v\in\text{round 1}\Rightarrow \lane(u)=\lane(v)\)	pass · 0 of 114 edges
I2 provenance	every parent exists; every step is in its agent's verbatim return	pass
I3 time order	\(u\to v\Rightarrow t(u)\le t(v)\)	fail · 3 of 276 edges e.g. A3-4 (02:07) cites A3-3 (02:40)
I4 budget	\(\|\mathcal A\|\le 9\)	pass · 8
I5 audited before use	\(R\) cites a proved \(u\) at time \(t\Rightarrow\exists\,w\): \(u\to w\), \(\lane(w)\ne\lane(u)\), \(t(w)\le t\)	fail · 4 of 14 inputs 3 are the auditor's own summaries
I6 labels	every step has a kind and a status from the schema	pass

What each invariant means

The invariants of in words.
invariant	in words	why a correct run needs it
I1 independence	in round 1, a step cites only steps by its own agent	round-1 agents must not see each other's work; only then is agreement between two of them evidence
I2 provenance	every cited step exists, and every step appears word for word in the return its agent sent	the root may record steps, not invent or reword them
I3 time order	a step cites only steps written before it	a result cannot be used before it exists; a failure means the timestamps cannot be trusted
I4 budget	at most 9 agents in the run	the skill's cost limit
I5 audited before use	when the root uses a step \(u\) marked proved, a check, objection or verdict \(w\) by a different agent already cited \(u\)	no result is relied on on its author's word alone
I6 labels	every step has a kind (idea, lemma, computation, check, …) and a status (proved, partial, …) from a fixed list	the scripts and pictures read these labels; a free-form label cannot be checked

Result: the run was independent and traceable, but its clocks and its use of unchecked results were not; the verified design adds I7–I8 and checks all of them during the run.