The mission
Search mathematics for what makes AI safe. Build it. Publish it.
AI agents now take actions. They approve applications, quote prices, send offers, and move money. The question that matters is whether the reasoning behind each action holds together, and whether anyone can show that afterwards.
Mathematics already has answers to parts of that question. Some sit in branches nobody has connected to AI yet. Sheaf Labs looks for them, tests them on live agents, and ships the ones that work as products. Every method we ship is published, so the number it produces can be checked by anyone.
What we claim: we measure whether the information an agent is about to act on agrees with itself, and stop the action when it does not. It is one tool. We are looking for the next.
In production
Three branches of mathematics, each one a product you can run today.
Each measures a different way that a group of agents can fail to agree. One number comes out. It is computed the same way every time.
Sheaf cohomology
The mathematics of whether local pieces fit into one whole. Each agent is sure of its own piece and cannot see the rest. H⁰ is what every agent agrees on. H¹ is a contradiction that lives only in how the pieces fit together, and in no single piece.
What you getContradictions that checking two agents at a time would miss. The agents' claims are compared around every loop, and a loop that cannot close is named.
See it run live →Spectral graph theory
The sheaf Laplacian. Agents and their claims form a graph. Disagreement becomes energy on that graph, and the graph's spectrum says how stable the consensus is and which claim carries the conflict.
What you getA coherence score from 0 to 100, the consensus answer the agents' confidence supports, and a robustness read on it. It points at the claim the disagreement is about.
How it is computed →Formal logic
A complete solver decides whether a set of rules can all hold at once. If they cannot, it names the smallest set that clash. Rules that mix arithmetic across fields go to an SMT solver.
What you getRules written in plain English are checked for hidden contradictions before they govern an agent. A deep chain of implications is found with the same certainty as a direct clash.
Write rules in plain English →Under study
What we are testing next.
Each of these is a known piece of mathematics that has not been applied to agent safety in a product. Each one is tested on live agent traffic before it ships. The ones that add a check you could not get otherwise will.
- λ₂Spectral clustering on the Laplacian we already build.
Which subset of the agents forms the other camp, on top of the score that says they disagree.
- ± 4Confidence bounds on the score.
Report "coherence 82, plus or minus 4" and whether the difference from last time is real.
- H(p)Information theory.
Tell a clean two-camp split from a spread of unrelated answers. Both score low today. They mean different things.
- BelBayesian and Dempster–Shafer evidence combination.
Reconcile claims by how much each agent has earned the right to be believed.
- Ȟ¹The cohomology of contextuality.
A certificate that no single consistent world explains all of the agents' answers at once. The same mathematics that describes why quantum measurements cannot be explained classically.
- βPersistent homology.
Contradictions that survive as you zoom out, separated from ones that are noise.
- ∀xPredicate calculus over the ledger.
Rules with quantifiers, over every applicant and every case, beyond the yes-or-no rules of today.
Published
The method is on the record.
A number you can check beats a claim you have to take on trust. The mathematics behind every Sheaf product is published with a permanent DOI, and a provisional patent is filed.
Why mathematics
You could build a check. The hard part is knowing when your check is wrong.
Any team can score agreement between agents. The question is what the number means when something has gone wrong underneath it. Ours failed open once: no agent had been measured, the score came back 100, and an action was approved. We found it in our own verification run against production. The mathematics says what the number must be when nothing was measured, and the number did not match, so the fix was clear: the gate now refuses an unmeasured panel.
That is what the mathematics buys. It says what the answer has to be, so a wrong answer is visible. A check built without it can only tell you what it saw.
Much of Sheaf's code is written with AI assistance, and some readers will ask what that means. The mathematics the products run on is written in Lean and checked by machine, and the files are public. See what is proved, and what the proofs leave out.