Proof Kernels Are the New Agent Managers

The hardest part of deploying AI agents is no longer getting them to produce work. It is deciding when that work is allowed to become real.

A coding agent can draft a patch before a senior engineer has finished reading the ticket. A compliance assistant can assemble a report before the risk team has found the right template. A workflow agent can call APIs, move records, send messages, and update systems in a sequence that looks coherent in the transcript. The speed is useful. It is also the reason traditional review breaks down. Human managers cannot inspect every intermediate artifact at agent speed and still run the business.

That makes a recent arXiv paper, AI with Authority, from Application to Silicon, worth reading beyond its hardware-design headline. Jason Hickey reports a five-week project in which one researcher directed a small fleet of AI agents from application code through a verified compiler and executive to a RISC-V processor taped out on a community silicon shuttle. The abstract is intentionally striking: no RTL was written by a human, and no proof passed through human review. The project’s discipline, called Salt, rested on a proof kernel — a machine-checking layer where mathematical claims had to pass as formal artifacts rather than persuasive prose.

The enterprise lesson is not that every company should immediately formalize its whole software stack in Lean 4. That would be fantasy for most teams. The more useful lesson is narrower and more operational: as agents gain authority, the organization needs checkers that are harder to fool than the people reading the transcript.

A proof kernel is the sharpest version of that idea. In a theorem-proving environment, a proof is not accepted because it sounds reasonable. It is accepted because a small trusted checker can verify that the claimed theorem follows from the allowed rules. Hickey’s paper frames that as the difference between reviewing agent output and governing agent authority. The human sets statements, designs, and rulings. The machine checks whether the artifacts that agents pass between one another are admissible.

Most production teams will not start with theorem proving. They should still copy the pattern.

The pattern is: put a deterministic gate at the boundary where agent output becomes authority. A schema validator before a compliance artifact leaves draft mode. A type checker before generated code moves forward. A migration dry run before a database change. A simulator before an operations agent touches live infrastructure. A policy engine before a customer-facing message is sent. A property test before a pricing or eligibility rule ships. In narrow domains where correctness can be formalized, a proof assistant or equivalence checker may be the right gate. In many domains, a humbler checker is enough.

The point is not to prove everything. It is to stop pretending that a polished explanation is the same as a verified artifact.

This distinction matters because documentation-shaped output can look safer than it is. Another August 2026 arXiv paper, From Regulation to Implementation, studies LLM-assisted regulatory compliance artifacts for industrial contexts. Its abstract reports a split that should sound familiar to anyone building enterprise AI: stricter formatting can make outputs more consistent, but may still lead to hallucinations; less strict formats require more context to maintain completeness and consistency. Templates help. Higher-context prompts help. Neither turns a generated document into evidence by itself.

That is the trap. Many organizations respond to agent risk by adding more instructions, more checklists, and more review text. Those are useful, but they are not the same as a control plane. A control plane needs something that can reject a claim even when the prose is fluent, the citation list looks plausible, and the agent is confident.

For a healthcare workflow, that might mean a minimum-necessary rule enforced by code before any patient-related message is assembled. For a finance workflow, it might mean a reconciliation check that blocks posting if the ledger does not balance. For software delivery, it might mean generated patches must pass tests that encode the business invariant, not just lint. For internal knowledge work, it might mean every answer that influences a decision must carry source spans and fail closed when evidence is missing.

The key design move is to separate two questions that agent transcripts often blur together.

First: did the agent produce something that sounds like the requested work?

Second: did an independent checker accept the part of that work that gives it authority?

The first question is subjective and language-heavy. The second should be as mechanical as the domain allows. When those questions are merged, organizations end up with managers reading long traces and making vibes-based calls under time pressure. When they are separated, human review becomes more strategic. People decide what the system is allowed to do, which boundaries require evidence, and which checker is trusted for each boundary.

This also changes how teams should think about agent observability. Logs and traces are necessary, but they are often retrospective. They tell you what happened after the agent acted. Proof kernels, validators, simulators, policy engines, and equivalence checks are prospective. They decide what is allowed to happen next. The strongest agent systems will use both: traces for accountability and learning, gates for authority.

NIST’s AI Risk Management Framework gives teams a useful governance vocabulary: govern, map, measure, and manage. Agent checkers make that vocabulary concrete. Mapping identifies where the agent can create side effects. Measuring defines what evidence is required at each boundary. Managing means the system can actually block, reroute, escalate, or roll back when the evidence is absent or invalid. Governance stops being a slide and becomes a set of enforced transitions.

There is also a culture shift here. Teams tend to ask whether an agent is smart enough for a workflow. A better question is whether the workflow has been shaped so that the agent’s important claims can be checked. If not, adding a stronger model may only make the unsafe path faster and more convincing.

A practical starting exercise is simple. Pick one agent workflow and list the moments where output becomes authority: a file is written, an API call is made, a customer sees a message, a record changes status, money moves, access expands, or a human is asked to approve a recommendation. For each moment, ask: what artifact would make this action checkable? What tool can reject it? What happens when the check fails? Who owns the checker?

That exercise will not produce a proof kernel overnight. It will produce something almost as valuable: an authority map. Once the map exists, teams can decide where ordinary validation is enough and where stronger verification is worth the investment.

The next generation of agent management will not be a bigger prompt telling agents to be careful. It will be a stack of gates that make care enforceable. Humans will still own intent, priorities, exceptions, and judgment. But wherever an agent’s claim can be converted into a machine-checkable artifact, it should be.

That is the durable lesson from proof kernels. They are not just a formal-methods curiosity. They are a preview of how serious organizations will grant AI systems authority: not because the agent explained itself well, but because the claim survived a checker that does not care how confident the agent sounded.