Skip to content
Products
Knowledge Hub
Company
Sign in
Request a demo
How verification works at Ascendr

Verifiable does not mean infallible.

It means the system tells you what was inferred, what evidence supports or contradicts the result, what was checked, what the check establishes, and what remains a human decision.

Five principles for high-stakes AI

I

Evidence over assertion

Consequential claims link to inspectable sources.

II

Boundary over blanket assurance

The output identifies what was checked and what was not.

III

Formal methods where structure permits

Deterministic or formal checking replaces probabilistic reasoning where the representation is explicit enough.

IV

Uncertainty made usable

Estimates, conflicts, calibration, and abstention are visible.

V

Human responsibility preserved

The system supports a named decision owner rather than obscuring accountability.

From unstructured material to an assurance record

1
Collect

Collect evidence and provenance.

2
Represent

Represent the claim, dependencies, constraints, or event in a typed structure.

3
Propose

Use models to propose interpretations or mappings.

4
Check

Apply the appropriate checker to the structured portion.

5
Record

Record support, contradiction, assumptions, limitations, and status.

6
Decide

Proceed, narrow, request more evidence, escalate, or abstain according to policy.

Formal verification

What a machine-checked proof does, and does not, establish.

A Lean 4 certificate can establish that a named proposition follows from formal definitions and recorded premises. The kernel checks the proof term; an axiom audit identifies additional assumptions. That is a strong guarantee about the formal computation. It is not a guarantee that natural-language interpretation, source evidence, legal doctrine, or real-world inputs were encoded correctly.

formal_result_disclosure
Proved
Name the proposition in plain English and formal notation.
Given
List the encoded inputs, premises, definitions, and hashes.
Checked by
Lean version, project commit, kernel re-check procedure, axiom audit.
Not proved
List semantic, evidentiary, legal, forecasting, and human-judgment questions outside the theorem.
Reproduce
Link to the artifact, lockfile or container, commands, and expected output.

Different decisions require different assurance.

AtlasResearch and expertise intelligence
Evidence-grounded profilesDeterministic eligibility or coverage checks where configuredEstimated relevanceHuman-owned selection
TracePatent claim analysis
Evidence-linked mappingsDeterministic graph checksFormal certificates for eligible named computationsCounsel-owned legal conclusions
SentinelTechnology intelligence
Source-linked observationsCritic-reviewed interpretationsPolicy-based alertsEstimated forecasts evaluated over time
Published technical milestone

A machine-verified coverage core for a hybrid patent-analysis pipeline.

Ascendr's published patent-analysis work includes a Lean 4 coverage-core generator that is machine-verified once bounded match scores are fixed. The paper separately classifies specification-level results, architecturally checked candidate certificates, and inputs below the trust boundary. Its case study is synthetic, and validation against adjudicated cases is future work.

Read the paper and verification-status table
What we are building toward

A standardized assurance record across Ascendr products.

Our direction is to make every consequential output carry a consistent record of evidence, contradiction, checks, premises, uncertainty, versions, and accountable review. We will publish status and validation evidence as components move from research to production.