proveml
Every claim an AI writes, checked against your data and your rules.
AI is genuinely exciting right now. Every few months it writes better, reasons further, picks up more of the work that used to eat your afternoons. You start to feel foolish for not using it.
Then it turns on you. Quietly, in the middle of a perfectly ordinary sentence:
Hi Marta, thanks for reaching out aboutorder 4821. It ships on14 March, and your warranty runs until3 June 2027. You are still covered, so the repair is free of charge. The outstanding balance is€1,240.
- subject
- verified
- falsified
- a judgment
- unproven
Send that as it stands and you have promised a year of warranty you do not owe, and quoted a figure that came from nowhere. Marta will hold you to both, and she will be right to — she was told in writing.
One mail, four kinds of truth, and without the marks they all read the same: fluency is uniform, correctness is not. Unproven is the one to sit with — most systems collapse it into silence, and that is how a made-up number ends up reading like a checked one.
Every chat window warns you about this — AI can make mistakes, check important info — and none of them tells you how. Check what, against what, by hand, every number, every time? The disclaimer hands you the responsibility and no instrument to carry it. And it gets worse as the models improve: at 97% correct you stop looking, so the rare wrong number travels further. Accuracy without a way to check does not remove the risk. It hides it.
So the check has to become mechanical. Not a second AI grading the first — that is another opinion, and opinions can be talked out of things. A lookup. A comparison. Something that either matches your data or does not.
the disclaimer is not the problem · the missing instrument is
Maximum determinism, without caging the model.
The obvious fix is to lock the model down: templates, fixed sentences, dropdowns of approved phrasings. It works, and it throws away the reason you wanted a language model. You get a mail-merge that costs GPU time.
ProveML pulls the two apart. Generation stays fully open — the model writes what it wants, in whatever order, in any language, at any length. Verification stays fully closed — every claim it marks resolves to one path in your data and is checked by string equality or arithmetic, with no model anywhere in that loop.
Open-endedness where it pays, determinism where it counts. The prose is free; the claims are not.
First the store is vouched for: signed off by a reader, attested by an issuer, or recomputed from a ledger. Then every claim is checked against it.
Two pictures, one model. Above, it reads the sources and proposes a reading per value, and a person signs each one: that is where the store comes from. Below, the same model writes against that signed store, and the verifier checks every claim against the same data it was given, not against a second opinion. One box can invent, one can judge, the rest look things up. Put the verifier in front of an action instead of a report and the same check becomes a gate: nothing runs until its claims hold.
The verifier never does arithmetic, and never asks what today is. A check that knows the date gives a different answer tomorrow for the same text, and then it is not a proof. Your data layer works out warrantyDaysLeft and stores it; the verifier only compares it to zero. Everything it touches is a value someone can point at.
What the model actually writes.
Nothing above was styled by hand. This is what the model wrote, and the marks come from checking it:
Hi Marta, thanks for reaching out about @[order:4821]{order 4821}. It ships on %[shipDate]{14 March}, and your warranty runs until %[warrantyUntil]{3 June 2027}. ?[covered: IS_IN_WARRANTY]{You are still covered}, so the repair is free of charge. The outstanding balance is %[balance]{€1,240}.
Strip the brackets and you have the mail, word for word. What was added is a path into your records wrapped around the words the reader was going to see anyway. Renderers that do not know ProveML pass them through unchanged; a verifier that does resolves every one against your data. warrantyUntil came back wrong because the order says 2026. balance came back unprovable because orders in this system have no balance field at all — the model filled a plausible gap, which is exactly what models do.
Neither failure needed a human to notice it, and neither needed a second AI to judge it. A lookup was enough.
Which raises the obvious question: how does the model know to write any of this? You do not teach it. The package generates the system prompt from your own store and registry, so the field names it sees are the ones the verifier will resolve — hand-written instructions go stale the moment a field is added, and then the model names something the verifier cannot find. Told only what the constructs are, Claude Opus 5 got 86% of its claims verified on the first pass; with the binding and cutoff rules the generated prompt adds, 100%.
Change the record. The marks follow.
This is not a picture of the output. It is proveml from npm, running in this page against the record beside it. Edit a value and the reply is judged again, mark by mark. Nothing is sent anywhere: the check happens in your browser.
what goes back to the model
the record
There is no balance field on an order in this system. That is why the figure in the last sentence can never turn green: it is unproven, not wrong.
Set warrantyUntil to 2027 and the line through it clears: the mark was computed, not painted on. Set warrantyDaysLeft to 0 and the judgement that follows from it fails, while the sentence around it stays exactly as fluent as it was.
What it lets you do.
Send without rereading
Every value carries a status before anyone sees it, so your attention goes to the handful that failed instead of the hundred that held.
Agents that fix themselves
A failed check is a specific message —warrantyUntil is 3 June 2026, not 2027 — so the model repairs that one claim and tries again. No human needed for the boring half.
Check what you did not write
Verification is separate from generation, so a document can be checked months later, against the data as it stood, with the same answer every time.
Adjectives that mean something
“Still covered” means what your warranty rule says it means, defined outside the model. The phrase becomes a claim you can check, not a courtesy.
Evidence on request
Audit view puts the checked path beside each claim —
order:4821.shipDate— so a reviewer sees which record backs which sentence, without reading any markup.Names stay with you
The model works with
order:4821; real names and addresses are filled in at render time. The claims are checkable, the personal data never left your side.
A failed claim is a correction, not a rejection.
A failed check comes back as a correction: the path it looked up, the value the model wrote, and the value the record holds. That is enough to repair one sentence and try again. How many rounds is the caller’s choice, and each one costs a call. What matters is what happens when they run out: a claim that stays unproven is not quietly dropped and does not block the text. It ships with its mark on, so the reader sees exactly which part nobody could stand behind.
the model writes · the verifier answers with paths and values · the model fixes that one claim · what stays unproven ships marked, never silent
the reference: syntax, fact store, signed sources, cli →
Some links are not lookups.
Everything above checks a claim against a record. But whether that record is a fair reading of the source it came from is not a lookup, and no amount of determinism turns it into one. Someone has to read the quote and say yes, that is what it says.
So those judgements get the verifier’s discipline instead of a spreadsheet. A judgement is stored under a hash of exactly the content it approved. Change the wording, the value or the source and the judgement does not travel with it — it turns up as an orphan: a checkmark that would have gone on lying quietly on a hand-kept list.
Evidence comes in three kinds, named rather than blurred: a quote, checked verbatim against the archived source; a value derived from one; or an absence, which is a finding too. Whoever signs the finished review attests to it and cannot change a verdict — the same split that keeps a model out of the verification loop, applied to people.
a human judges · the judgement is bound to what it judged · edit the source and the checkmark dies with it
What it does not do.
ProveML verifies that claims match your data — not that your data is right. If the source is wrong, the verified claim is confidently wrong; the review layer above is how evidence gets under the data, and it works because a human read the source, not because the machine did. It checks what is inside the markup; prose outside stays unchecked, on purpose — and the marking itself is the model’s work, so a number written without markup passes as prose. Coverage is the one thing the verifier cannot judge for you. And values must match exactly, so a report says 18.5, not “about 18”.
We would rather state that plainly than sell certainty we cannot deliver. It is the same reason the verifier has no model in it: a guarantee you can explain in one sentence is worth more than one you have to trust.
Where it runs.
ProveML runs under Elixir, our watchful agent: every weekly report it sends is proven before it reaches you. It is the mechanical half of our trust standard — the part that does not depend on us keeping a promise. The research behind it is written up in a paper, with the benchmarks and experiment artifacts published alongside, and the credential work connects it to the European identity infrastructure we spent years building.
the findings, verified by ProveML itself → · read the paper (pdf) → · the framework behind it →