Governing AI Agents with an Evidence System: A Governance Practice for Formally Verified Crypto Code

When AI agents start writing crypto code that requires formal verification, directing them by "does this feel right?" is roughly equivalent to running blindfolded through a minefield. An "evidence system" approach proposed by a developer on Reddit makes governance, not intuition, the core mechanism of human-AI collaboration — and the framing deserves serious scrutiny, because it touches on a dimension that most AI coding discussions overlook: in domains where correctness is non-negotiable, how do we make AI output auditable, traceable, and refutable?

Why "Vibes" Fail in Formal Verification Contexts

Formally verified crypto code has a distinctive property: it doesn't aim for "runs without errors" but for "satisfies the specification under all possible inputs." This means the traditional software engineering loop of "write tests, they pass, merge" doesn't hold here — passing tests are a necessary condition, nowhere near a sufficient one.

AI agents amplify the risk in this setting. A model that can fluently generate code can equally fluently generate proof scripts or invariants that look correct, and human reviewers are easily persuaded by surface-level coherence. The original title's use of "vibes" pinpoints this danger precisely: when the basis for judgment degrades from evidence to familiarity of tone and format, collaboration becomes a gamble.

The value of an evidence system is that it replaces "I trust this output" with "what verifiable support does this output come with?"

Formal verification refers to techniques that use mathematical methods to prove that a program or system satisfies a precise specification, commonly including theorem proving (e.g., Coq, Isabelle), model checking, and abstract interpretation. Unlike testing, it does not sample a finite set of inputs but attempts to cover all possible behaviors, and can therefore conclude by exhaustive argument that "no counterexample exists." The price is a very high barrier: developers must first write a formal specification, then construct machine-checkable proof scripts, and any deviation in a definition can render the entire proof meaningless. Crypto protocols often adopt formal verification because their failures tend to be silent security breakdowns rather than crashes, and once deployed they are nearly impossible to patch after the fact. This also explains why AI-generated proof drafts that "look self-consistent" are especially dangerous — judging the correctness of formal verification itself requires deep professional judgment, and there is a vast gulf between surface-level syntactic plausibility and a genuinely checkable proof.

The Core Structure of the Evidence System: Making Every AI Output Carry Its "Burden of Proof"

According to the Reddit discussion, the key to this mechanism is not any particular tool but a set of workflow conventions: every substantive change by an AI agent must come with an independently reviewable chain of evidence, rather than the conclusion alone.

Specifically, evidence includes at least several layers:

• Specification mapping: Which formal specification does this code or proof correspond to? Does the change alter the scope of specification coverage?
• Verifier output: The actual run results from formal verification tools (such as theorem provers or model checkers), not the AI's paraphrase of those results.
• Counterexample search record: What the agent did, found, and ruled out when attempting to construct inputs that violate the specification.
• Explicit declaration of uncertainty: Which parts the agent cannot provide evidence for and that require human intervention.

The essence of this structure is an "inversion of the burden of proof" — rather than humans proving the AI wrong, the AI must first prove that it has grounds to be considered correct. This dramatically reduces the reviewer's cognitive load and strips "looks reasonable" of its persuasive power.

Invariants are assertions that always hold true during program execution, and are one of the most commonly used forms of specification in formal verification and program reasoning. For example, in the state machine of a crypto protocol, "the length of the negotiated key always equals the security parameter" is an invariant. Developers argue for the system's security properties by proving that the initial state satisfies the invariant and that every state transition preserves it. The problem is that selecting and formulating invariants is itself a creative act: choose too weak an invariant and the proof passes easily but provides insufficient guarantees; choose too strong a one and it may be impossible to prove at all. AI agents can rapidly generate large numbers of candidate invariants, but a substantial portion merely "look like they express the right intuition" — in reality they may not be accepted by the verifier or may not cover the key risks. That is precisely why the evidence system requires agents to submit not only invariants but also the actual verifier results for them: to separate "does the invariant actually hold" from rhetorical persuasiveness and hand it over to reproducible machine checking.

The Governance Perspective: How the Human's Role in the Loop Shifts

Across multiple discussions, one recurring consensus is that the evidence system changes not AI's capabilities but the points at which humans intervene. Developers shift from "reading code line by line" to "reviewing the sufficiency of evidence" — judging whether the evidence an agent submits truly covers the risk surface and whether any verification steps were skipped.

This shift has practical benefits. Line-by-line review of AI-generated proof code is extremely attention-intensive and easily loses focus in long outputs; reviewing a structured evidence checklist, by contrast, lets limited human judgment concentrate on the higher-leverage question of "is this evidence trustworthy?"

There are points of disagreement too. Some discussants argue that an evidence system imposes a "ritualistic burden" on agents — the agent may learn to produce evidence that is formally complete but substantively hollow, creating a new kind of "evidence vibes." This concern is legitimate, and it shows that the evidence system itself needs to be governed: evidence templates must not be defined by the AI itself, and verifier invocations must be reproducible.

The concern about "ritualistic burden" raised in multi-source discussions is closely related to Goodhart's Law in software engineering: when a measure becomes a target, it ceases to be a good measure. If the format of the evidence checklist is defined by the party being reviewed, the agent may learn to produce formally complete but substantively hollow material — for example, citing verifier output that was never actually executed, or framing "no counterexample found" as "all counterexamples ruled out." Mitigating this risk typically requires several institutional design choices: evidence templates are fixed in advance by humans rather than generated by the agent; verifier invocations must record the command, version, and input hash so that a third party can independently replay them; and critical evidence should come from a different tool or model than the generating agent, forming a cross-check. In other words, the credibility of an evidence system depends not on the quantity of evidence but on its reproducibility and independence — which is also why it is called "governance" rather than a "prompting trick."

Implications for AI Coding Workflows

Even if you don't write crypto code, this approach has transferable value. Any AI-assisted coding scenario where "getting it wrong is costly" — safety-critical logic, data migration scripts, permission systems — can borrow the "evidence-first" principle: require the AI to provide a verification method alongside its solution, rather than waiting for humans to discover problems after the fact.

According to observations from a single source, the developer's practice also emphasizes the persistence of evidence: the evidence from every agent interaction is archived, forming a traceable decision history. This makes "why did we accept this change at the time" no longer a matter of memory but a queryable record.

From "vibes" to "governance" is fundamentally about transforming human-AI collaboration from a problem of trust into a problem of institutions. This shift may do more to determine AI's practical usability in serious engineering domains than any single model's progress.

One-line Summary

Replace intuition with an evidence system, making AI auditable and accountable in formal verification settings.

Paragraph Summary

The article examines an "evidence system" proposed by a developer on Reddit for governing AI agents in formally verified crypto code. The author notes that formal verification aims to satisfy a specification for all inputs — passing tests are far from sufficient for correctness — and that AI can fluently produce proof scripts that "look correct," easily swaying human reviewers. The core of the evidence system is an inversion of the burden of proof: every substantive change by an agent must include specification mapping, actual verifier output, counterexample search records, and uncertainty declarations, stripping "looks reasonable" of its persuasive power. The human role then shifts from reading code line by line to reviewing evidence sufficiency, focusing limited judgment on higher-leverage questions. The article also warns that the evidence system itself may become ritualized, requiring constraints on evidence templates and reproducibility of verifier invocations, and notes the approach transfers to high-risk scenarios such as safety-critical logic and data migration.