Every High-Stakes AI Answer Should Carry a Verdict

Confidence is not proof. In the final part of our verification gap series, we explain how machine-checkable certificates can make high-stakes AI outputs auditable and honest about their limits.

Imagine an AI system in a hospital that reads the available evidence and recommends a treatment. Among the documents it retrieves is the drug’s official label, which contradicts part of the recommendation. The system still recommends the treatment with 95% support because its score was designed to count supporting evidence, not evidence that disagrees.

The system is not deliberately hiding the conflict. It simply has no mechanism for representing it.

A second failure can arise from the wording of a question. Ask the same question in two different ways, and the retrieval result may silently change. An embedding similarity of 0.84 for one phrasing might become 0.71 for a paraphrase, with no warning that the answer now depends on a different set of documents.

These are not ordinary implementation bugs. They are structural consequences of AI pipelines that produce precise numbers without checkable guarantees. Our new research paper calls these outputs point estimates without theorems and proposes an architecture for addressing the problem.

Part 1 of this series named the verification gap. Part 2 showed how proof-carrying certificates can narrow that gap in patent analysis. This final part extends the architecture to the common components of high-stakes AI pipelines.

Verify the pipeline around the model:

The central idea is straightforward: let AI perform the work that genuinely requires language understanding, such as reading documents, retrieving evidence, and proposing answers or actions. Once that output becomes structured, hand the remaining computation to a deterministic system that can be independently checked.

The paper calls the dividing line between these two layers the trust boundary. The AI operates below the boundary. The structured checks and proof certificates sit above it.

The certificate makes a deliberately limited promise. It does not prove that a medical recommendation is correct, that a legal conclusion is sound, or that a financial decision will succeed. Mathematics cannot establish those facts from language alone.

Instead, the certificate proves that the system followed its declared rules. Evidence was counted as specified, thresholds were applied consistently, conditions were checked, and the remaining assumptions were made visible. It verifies the structured computation surrounding the AI, not the external truth of the AI’s answer.

Three certificates for three questions:

The architecture introduces three main certificate families, each addressing a different failure mode.

1. Does the evidence disagree?

A support-only system can miss evidence that contradicts its answer. The conflict-aware grounding certificate prevents that evidence from disappearing.

Each claim receives one of four statuses:

• Supported: The evidence supports the claim.
• Contradicted: The evidence argues against the claim.
• Contested: The evidence contains both support and contradiction.
• Unknown: The available evidence does not establish either position.

An emission gate then checks the weighted mass of contradicted and contested claims. If that mass exceeds the declared threshold, the system must block the full answer. The certificate proves that the gate followed this rule, subject to the declared claim-decomposition and evidence-classification assumptions.

2. Does the answer survive rewording?

A retrieval system should not silently change its evidence because a user paraphrased a question. The embedding-sensitivity certificate measures how far the query representation moves across a declared family of meaning-preserving paraphrases.

That movement is compared with the relevant decision margin. The result is a checkable envelope describing when a change in wording should not alter a downstream decision.

The guarantee applies only to the declared paraphrase family and measured input class. It does not claim stability against every possible rewording.

3. Is an action safe to execute?

Some AI systems do more than produce answers. They move files, modify records, call tools, or initiate actions that may be difficult to reverse.

The Hoare-style certificate defines a precondition and postcondition for each action. The LLM proposes the action, while the formal layer verifies the precondition, executes it through a typed executor, verifies the postcondition, and issues a certificate. These certificates form a trajectory that fails at the first unsafe step. A small deterministic, Lean-audited runtime permits or blocks side effects.

From individual checks to pipeline-level guarantee:

A sequence of confidence scores does not automatically become an end-to-end guarantee. An 87% score at one stage and a 92% score at another do not tell a reviewer what the complete pipeline can safely promise.

The paper takes a different approach. It defines how the gains and decision margins of individual pipeline layers can be combined into a pipeline-wide perturbation budget. In plain language, that budget describes how much variation the full pipeline can tolerate before a downstream decision may change.

The compiled artifact includes the two-layer base case. The general multi-layer form is specified as the next step in the formal development.

The paper also introduces the Maximal Certifiable Residue. When the complete answer cannot be certified, this operator identifies the largest subset that satisfies the declared constraints and records exactly which claims were removed.

The choice no longer has to be between releasing an unsupported answer and returning nothing.

One answer, four possible verdicts:

The paper brings these checks together in a record called the Universal Assurance Card. The card is designed to accompany each governed AI response and summarize its evidence, stability, scope, safety, residue, and provenance.

Most importantly, every card carries one of four verdicts:

• Certified: Every required certificate passes, and the output is released with its proof bundle.
• Partial: Some non-load-bearing layers remain unverified. Those gaps are named, and the deployment policy determines whether they are acceptable.
• Residue: The complete answer cannot be certified, but a smaller certifiable answer can be released. The card lists what was removed.
• Abstain: No answer is released. The card provides machine-readable reasons.

The Residue verdict may be the most practically useful. Instead of bluffing through a failure or refusing without explanation, the system provides the portion it can support and an auditable record of what it withheld.

It is abstention with receipts.

The Assurance Card is a summary and policy interface. It does not replace the underlying certificates. Its schema and consistency predicate are currently specified in Lean but have not yet been added to the compiled artifact. Promoting the card to a compiled module is a stated next engineering step.

What the pilots actually showed:

The paper tested the three certificate families on adversarial inputs rather than only on favorable examples.

Contradiction detection

The first pilot inserted contradictions into the HotpotQA public question-answering benchmark. At its best reported operating point, the conflict-aware certificate caught 100% of the injected contradictions while falsely blocking 6.4% of clean answers.

The cosine-similarity baseline reached the same 100% catch rate only by falsely blocking 26.6% of clean answers.

Paraphrase stability

The second set of pilots tested the embedding-sensitivity certificate on short adversarial questions and longer passages. The certificate’s central separation premise held in only 20 to 30% of the short-query cases but in 98 to 100% of the long-form cases across the tested edit combinations.

That difference matters. The result does not support a universal deployment claim. It identifies where the certificate appears useful and where its scope must be narrowed or tested further.

Agent safety

The third pilot placed an AI agent in a controlled filesystem sandbox containing injected unsafe actions. The Lean-checked action harness blocked 67% of those actions, compared with 28% for a regular-expression deny-list and 0% for an unaudited agent. It produced informative audit logs for every block and recorded no false blocks on the benchmark’s benign destructive proposals.

The result also missed the pilot’s strict 95% block-rate target. That failure did not invalidate the formal certificate. Every action that passed satisfied the predicates the system had declared. Instead, the audit exposed where the predicate set was incomplete and which conditions needed to be extended.

This is an important distinction. Auditable systems can turn a failed benchmark into a specific engineering task. An opaque score usually cannot.

What is proven and what is not:

The paper separates completed work, specified work, assumptions, and limitations.

• Compiled and kernel-audited: The Lean 4 artifact covers 22 certificate types across 46 audited declarations. Seventeen declarations are axiom-free. The remaining declarations depend only on the trusted set and explicitly named mathematical, cryptographic, or human and ML assumptions.
• No hidden proof shortcuts: The artifact contains no uses of sorryAx or Lean.ofReduceBool. 
• Specified but not yet compiled: The Universal Assurance Card and the general multi-layer compositional-stability result remain identified engineering steps.
• Conditional by design: The certificates verify structured computations based on declared inputs and assumptions. They do not prove that the underlying evidence or natural-language judgments are factually correct.
• Limited empirical scope: The pilots used HotpotQA and a controlled filesystem sandbox. Replication in patent and technical intelligence, legal retrieval, regulated finance, and clinical decision support remains future work.
• Outside the guarantee: A hallucination that remains stable across samples and agrees with a corrupted retrieval corpus may still pass. The architecture makes assumptions visible. It does not eliminate them.

We publish the research the same way we believe AI systems should publish consequential claims, with its boundaries attached.

Five questions to ask about any high stakes AI-system:

For anyone evaluating an AI system, the paper suggests a practical test:

1. Can the system show supporting and contradicting evidence separately?
2. Can it tell you whether rewording the question changes the evidence or result?
3. Are conditions checked before the system performs an irreversible action?
4. What happens when the complete answer cannot be certified?
5. Can an independent reviewer inspect the assumptions and replay the checks?

A confidence score alone cannot answer these questions.

Where this matters:

This architecture is intended for situations in which the cost of a wrong answer is significantly greater than the cost of checking it: patent and technical intelligence, legal retrieval, regulated finance, clinical decision support, and AI agents with irreversible side effects. It is not intended for creative writing or open-ended generation, where this level of assurance would add unnecessary weight.

For the research, IP, and technology teams Ascendr serves, the practical question is not simply, “How confident is the model?” It is, “What was checked, what remains conditional, and who is responsible for the decision?”

That principle is central to our work: preserve the evidence, surface contradictions, check what can be checked, label what remains uncertain, and keep human responsibility visible.

When output is cheap, trust becomes the work. This is what building that trust into an AI pipeline can look like.

Read the full paper here.

This is the final part of our three-part series on Verification Gap. Part 1 named the verification gap. Part 2 examined proof-carrying certificates for patent analysis. Read the complete series at https://ascendr.ai/library/

Written by the Ascendr Team

Ascendr, PBC is a public benefit corporation that believes every high-stakes decision deserves better than opinion. We wrote this series the way we build our products, with every claim traceable and every limit labeled. Through our writing, we share practical ideas that help research, IP, and technology teams make clearer, more defensible decisions.