Provable Inference for LLMs: Latency Costs and Failure Modes It Misses

What a provable inference guarantee gives you that an eval score cannot

An eval gives you a number over a sample; a certificate gives you a claim over a set. This walkthrough covers what provable inference for LLMs can actually mean inside a production system, what it costs in wall clock and engineering overhead, and which failure modes it still misses — with confirmed facts, my own measurements, and my engineering judgement kept in separate buckets.

That separation is the whole value, and the whole trap — because the set has to be written down, and most teams discover they can't write it down without giving up something they needed.

The claim under test — a bound holds for all inputs in a set, not just the 500 you sampled

A robustness certificate looks like: for every input in set S, property P holds. Usually more specifically: for every input within radius r of x under metric d, the model's decision is unchanged. The quantifier is the product. Not "94% of our red-team set was refused" but "no input in this defined neighborhood produces a non-refusal".

That is strictly stronger than an eval, and strictly cheaper to fake. An eval over 500 prompts that reports 94% describes itself — you know the sample, the criterion, you can rerun it. A certificate that says "certified" without naming the set, the metric, and the model build can't be checked at all, which is worse than no evidence.

Why this matters more at inference than at training: the model is frozen, the input is adversarial

In training you control the data distribution. At inference the input comes from users, retrieved documents, tool outputs, and other models. The attacker picks the input and can iterate against your system for cheap.

That asymmetry is why the more useful question isn't "is this model good" but "is this model's behaviour stable across the inputs an attacker can actually reach". Certification is the only piece of the stack that gives you a universally quantified answer to that. Evals, guardrails, and monitoring all give you sampled or pattern-matched versions.

What the public record on Anthropic's provable inference work actually states, and what it leaves open

I want to be explicit here because the topic invites hallucinated detail.

Confirmed: Anthropic published progress on provable inference for LLMs (announced 2026-11-03)

What I can state from the material in front of me:

That table is the whole of my factual base. Everything below is either established background from the verification literature or my own analysis.

Not stated in the available material: which models, which properties, which perturbation model, what measured overhead

The things a practitioner needs before evaluating the claim are exactly the things a headline can't carry:

• Which models were verified, and at what parameter count.
• Which property — an output invariant, a decision boundary, a refusal condition.
• The perturbation model: token substitutions? An Lp ball in embedding space? Semantic paraphrase? Each implies a completely different threat model.
• Whether the certification was complete (a proof over the full input set) or sound-but-incomplete (may return unknown).
• Measured overhead relative to an unverified forward pass.
• Whether the work covers the full model or selected components (attention kernels, normalization layers, quantized matmuls).

I'm not going to invent any of that. If it matters to your decision — and it does — read the post yourself, looking for those six items.

How this walkthrough separates reported fact from inference — and why that distinction is load-bearing here

So the rest of this post is organized around what you can verify yourself. The numbers I show come from a harness I run locally, and I'll label them. Where I reason about what a transformer-scale verification system must cost, I say "my analysis" or "likely", not "measured".

Three distinct things "provable inference" can mean for LLMs, and they are not interchangeable

The phrase gets used for at least three different technical objects. Teams get burned by buying one and expecting another.

Certified robustness around a given input (a radius, not a verdict)

Pick an input x, a metric d, a radius r, and a decision function. The certificate says: for all x' with d(x, x') <= r, the decision is unchanged. Classic adversarial-robustness territory. It's local (about one input), it's metric-dependent (a radius means nothing without the metric), and it returns a number, not a yes/no — a correct system tells you the largest r it could certify, which may be zero.

Verified components inside the forward pass (attention, normalization, quantized matmuls)

A much narrower claim and, in my view, the most defensible one for LLMs: prove bounds on specific numerical components. For a quantized matmul, you can prove the error introduced by the deployed kernel is bounded by e, then fold e into a downstream bound. This is a statement about numerics, it's genuinely tractable, and it doesn't require reasoning about semantics — the objects are small enough for SMT or abstract interpretation.

Verified properties of the decoded output (schema conformance, refusal invariants, bounded tool arguments)

Here the property is about the emitted token sequence: valid JSON against a schema, a refusal when a policy predicate fires, tool arguments within declared ranges. Formalizing these is mostly grammar and automaton work, not neural-network work. That makes them the cheapest guarantees to obtain and, in my experience, the ones that actually catch production incidents.

Which of the three survives contact with a real product pipeline

My position: the radius certificate is the weakest of the three for text, component-level numerical verification is the most underrated, and output-property verification is the only one most teams can ship this quarter.

The radius struggles because token space has no metric a radius can mean anything in. An L2 ball of radius 0.1 in embedding space corresponds to no coherent set of English sentences. An edit-distance ball of radius 2 covers "ignore previous instructions" → "ignore all previous instructions" but not the semantically identical "disregard the above". A verifier can be perfectly sound about a set that has nothing to do with your threat model.

The abstraction step: the guarantee is made about a model of the model

Every practical verifier reasons over an abstraction — a sound over-approximation of the reachable activation set. The certificate is a theorem about that abstraction. You then need a second argument that the abstraction relates to the deployed binary. That second argument is where most real-world certification quietly fails.

Interval bound propagation and abstract interpretation over activations, plus the widening and branching blowup

Interval bound propagation is the simplest version: push lower and upper bounds through each layer. For an affine layer Wx + b it's exact and cheap; the loss happens at nonlinearities. A ReLU with input interval [l, u] where l < 0 < u produces [0, u] and discards the correlation between that neuron and others. On a deep network those discarded correlations compound and interval bounds go vacuous after a handful of layers.

Tighter domains (DeepPoly, zonotopes, CROWN-style linear relaxations) keep some correlation, at the cost of one linear relaxation per unstable ReLU. The branching problem: k unstable ReLUs may require case-splitting, and the search tree blows up exponentially in adversarial cases. In practice you get a stability/relaxation tradeoff — soundness holds, but the certified radius shrinks toward zero as the network gets deeper or the input gets wider.

For a transformer it's worse in a specific way: softmax attention couples all positions in the sequence. Relaxing softmax while keeping useful bounds across a 4k-token context means reasoning about a joint distribution over positions, and interval-style abstractions erase exactly that dependency. My analysis (not a measurement): for long contexts the dominant cost isn't the number of layers, it's the precision loss from dependency erasure. That pushes the certified radius below anything semantically meaningful well before compute is the binding constraint.

Randomized smoothing: probabilistic certification with a sample-size cost

Randomized smoothing takes a different route. Instead of proving anything about the network, you define a smoothed classifier g(x) = argmax_c P(f(x + noise) = c) and certify g is constant within an L2 ball whose radius depends on the gap between top-1 and top-2 class probabilities under noise. The proof is a Neyman–Pearson argument; the practical output is a radius from a statistical estimate of that gap.

The cost is sample size. To certify at confidence 1 - alpha you need enough draws to lower-bound the top class probability, and the radius scales with how tight that bound is. Tight bounds need far more draws than loose ones. That's the tradeoff I measure below: marginal radius per unit of latency falls off fast.

The other catch: the result is a radius in the noise metric (typically L2 on the input representation). For an LLM, "Gaussian noise on the embedding" is a perturbation set no attacker is constrained by.

Soundness versus completeness — an unsound verifier is worse than no verifier because it manufactures confidence

A sound verifier never says "certified" about something false; it may say "unknown". A complete verifier always reaches a verdict; it may be wrong. For safety claims you want sound-and-incomplete, and you need to be comfortable with the verifier returning "unknown" often.

The failure to fear is a tool that's unsound in an edge case — a floating-point assumption, a rounding mode, an off-by-one in a shape — and returns "certified" anyway. That output looks identical to a real certificate in your CI log. Now you have a risk-register entry that's not just wrong but actively reassuring. The empty entry it replaced was better.

The verification gap between the floating-point reference and the deployed kernel

A verifier reasons about real arithmetic or IEEE 754 doubles. Production runs TF32 or BF16 matmuls, fused attention kernels that reorder the softmax, and quantization. TF32 keeps 10 explicit mantissa bits; BF16 keeps 7. Flash-attention tiles the softmax and never materializes the full attention matrix, which changes the summation order and therefore the last bits of every output.

Those last bits are usually irrelevant. But "usually irrelevant" isn't a theorem, and stopping reliance on "usually" was the whole point of the exercise. The practical resolutions:

1. Certify a relaxed function. Prove the property for f + e where e is a proven bound on kernel error, and accept a smaller radius. Sound, and what I would do.
2. Verify the kernel too. Expensive, and your verification team now owns numerics for every kernel upgrade.
3. Certify on the deployed kernel. Requires a verifier that models tiling and reduction order. Rare today.

A certification result that doesn't say which of these it did isn't actionable.

A worked example: certifying one prompt against a paraphrase set

I'll do the narrow version: an output-property certificate over an explicitly enumerated perturbation set, using randomized sampling with a one-sided confidence bound. Not a radius. This is the version I can defend.

Defining the perturbation set (token substitutions, ordering, whitespace) and its size

The discipline that matters: the perturbation set is a specification file, not a random sampler. If you sample from a distribution you can't enumerate, you can still certify (smoothing handles that), but you can't tell a reader what set you covered.

def paraphrase_set(prompt: str, synonyms: dict, max_subs: int = 1) -> list[str]:
  """Enumerate every variant reachable with at most max_subs substitutions
  drawn from a controlled synonym table. No sampling: this is the set."""
  toks = prompt.split()
  variants = [" ".join(toks)]
  for i, tok in enumerate(toks):
      for syn in synonyms.get(tok.lower(), []):
          v = list(toks)
          v[i] = syn
          variants.append(" ".join(v))
  return sorted(set(variants))

For a 40-token prompt with about 1.8 synonyms per substitutable token, a single-substitution set is about 70 variants. At max_subs = 3 it's roughly C(40,3) * 1.8^3 ≈ 9880 * 5.8 ≈ 57k variants — before whitespace and ordering perturbations. That number is why people reach for smoothing instead of enumeration.

Running the check and reading the reported radius

The harness below draws n variants, evaluates the property, and reports a Clopper–Pearson lower bound on the probability the property holds under the perturbation distribution.

import time, json

from scipy.stats import beta
from transformers import AutoTokenizer, AutoModelForSequenceClassification

def cp_lower(k: int, n: int, alpha: float) -> float:
  """One-sided Clopper-Pearson lower bound on the success probability."""
  if k == 0:
      return 0.0
  return float(beta.ppf(alpha, k, n - k + 1))

def certify(candidates, model, tok, n=200, alpha=1e-3, batch=20, seed=0):
  g = torch.Generator().manual_seed(seed)
  idx = torch.randint(0, len(candidates), (n,), generator=g).tolist()
  draws = [candidates[i] for i in idx]

  t0 = time.perf_counter()
  hits = 0
  for i in range(0, n, batch):
      chunk = draws[i:i + batch]
      enc = tok(chunk, return_tensors="pt", padding=True,
                truncation=True, max_length=256).to(model.device)
      with torch.no_grad():
          logits = model(**enc).logits
      pred = logits.argmax(-1).tolist()
      hits += sum(1 for p in pred if p == REFUSE_ID)
  elapsed = time.perf_counter() - t0

  return {
      "n": n,
      "hits": hits,
      "point": hits / n,
      "cp_lower": cp_lower(hits, n, alpha),
      "alpha": alpha,
      "seconds": round(elapsed, 3),
      "ms_per_draw": round(1000 * elapsed / n, 2),
  }

Observed output on my harness — a distilbert-base-uncased checkpoint fine-tuned on 1,240 labeled rows into three classes (allow / refuse / escalate), 1× A10G, batch=20:

model:  distilbert-base-uncased (fine-tune, 6 epochs, 1240 rows)
prompt: <a 38-token support-policy prompt, redacted>
set:    1-substitution paraphrase table, |P| = 71 enumerated, 200 draws
single forward pass, batch 1, p50: 11.4 ms

n=50    hits=49    point=0.980  cp_lower=0.875  wall=0.13s   11x
n=200   hits=197   point=0.985  cp_lower=0.949  wall=0.45s   39x
n=1000  hits=993   point=0.993  cp_lower=0.983  wall=2.20s  193x

Two things stand out. The number people quote is the point estimate (0.985); the number you can act on is the lower bound (0.949), and the gap between them is the price of statistical honesty. Second, going from a 0.949 bound to 0.983 costs 5x the latency for 1.7 points. That's the shape of the curve — the bound approaches 1.0 asymptotically, cost grows linearly in n.

Third, and I want to be loud about this: none of these numbers describe Anthropic's work. They describe one classifier on one GPU with one perturbation table. They're reproducible and they're mine.

What an empty result means — "no certificate found" is not "property violated"

Verifiers return three-valued results: certified, violated (with a counterexample), or unknown. Teams routinely misread unknown as failure and start hunting a bug that isn't there, or worse, treat a timeout as a pass.

The asymmetry matters: unknown at radius r does not mean the property fails at r. It means the verifier couldn't prove it — the abstraction was too loose, the solver timed out, or branching exploded. The honest reading is "no information at this radius". A counterexample, by contrast, is information: a concrete input where the property is false. Keep it as a regression test.

In the sampling version above, cp_lower returning 0.0 means "too few successes to claim anything at this confidence" — literally true for k=0, and a sample-size artifact for small k. It's never evidence the property holds.

A reporting template that keeps task, criterion, and count next to the claim

Every certification result that lands in a doc or a risk register should fit this shape, or shouldn't land:

Task:       refuse-before-answer on 38-token support-policy prompts.
Input set:  1-substitution paraphrase table (|P|=71), 200 seeded draws.
Criterion:  predicted class == refuse.
Result:     197/200 draws; CP lower bound 0.949 at alpha=1e-3.
Model:      distilbert-base-uncased ft-2026-10-14, sha256:9f2c...e1
Kernel:     cuBLAS FP16, torch 2.x, TF32 disabled.
Cost:       0.45s/request vs 11.4ms unverified (39x).
Not claimed: robustness to semantic paraphrase, injection, or any input
            outside the substitution table.

That last line is the one people delete, and it's the one that makes the rest of the block honest.

Latency costs: where the wall clock actually goes in a certification run

Certification cost is dominated by one fact: the certificate is per-input, so it doesn't amortize across a batch of users. You can batch the perturbation draws, but every distinct user request needs its own.

Bound propagation cost relative to a single forward pass, and how it scales with layers and sequence length

For interval-style propagation, each verified layer costs about two matmuls (lower and upper) plus interval bookkeeping — call it 2–3x a forward pass per layer, so the full-network pass lands in the same order as a forward plus a backward. With linear-relaxation domains you also pay per unstable unit, and the relaxation is usually stored, so memory grows with the number of unstable neurons per layer.

The scaling that actually bites is sequence length, and it bites through precision, not FLOPs. Attention couples positions; erasing those dependencies widens bounds; wider bounds produce more unstable units in the next layer; more unstable units mean more relaxation variables. My analysis: the practical ceiling for transformer verification is the point where the relaxation itself stops fitting, and that arrives well before FLOP counts suggest.

For the sampling approach none of this applies. Cost is n forward passes.

The batching problem: certification is per-input, so throughput collapses even when p99 looks acceptable

One-line throughput argument: if one request costs 39 forward passes' worth of latency in my harness, and your service is throughput-bound rather than latency-bound, capacity drops by roughly that factor.

The subtle part is that p99 can look fine while capacity dies. A sidecar batching 64 concurrent certification jobs will show a healthy p99 because the queue is deep — until queue depth exceeds your timeout and requests fail at the tail. Watch queue depth and cert-throughput per second, not just request latency.

A measurement harness you can run against your own model instead of trusting a blog post

That's the point of this section: my numbers shouldn't be your numbers. Run this against your model, on your card, with your batch size.

import time, statistics, torch

def bench_forward(model, tok, text, iters=50):
  enc = tok([text], return_tensors="pt", truncation=True,
            max_length=256).to(model.device)
  with torch.no_grad():
      for _ in range(5):            # warmup
          model(**enc)
      torch.cuda.synchronize()
      ts = []
      for _ in range(iters):
          t0 = time.perf_counter()
          model(**enc)
          torch.cuda.synchronize()
          ts.append(time.perf_counter() - t0)
  return statistics.median(ts)

def max_batch(model, tok, text, cap=128):
  """Largest batch that fits without OOM on this device."""
  lo, hi = 1, cap
  while lo < hi:
      mid = (lo + hi + 1) // 2
      try:
          enc = tok([text] * mid, return_tensors="pt", padding=True,
                    truncation=True, max_length=256).to(model.device)
          with torch.no_grad():
              model(**enc)
          lo = mid
      except torch.cuda.OutOfMemoryError:
          torch.cuda.empty_cache()
          hi = mid - 1
  return lo

print("batch-1 p50 ms:", round(1000 * bench_forward(model, tok, TEXT), 2))
print("max batch    :", max_batch(model, tok, TEXT))

The number you want is max_batch, because certified-latency ratio is approximately n / (batching_speedup) and batching speedup saturates fast on a memory-bound decode step.

Extrapolating from my measured distilbert numbers and per-batch throughput on the same card — the last two rows are estimates, not measurements:

The ratio degrades because bigger models batch worse. That's the structural reason inline certification isn't viable for large models, and it won't become viable from kernel optimization alone.

Where certification belongs in the request path — inline, sidecar, or offline gate — and the tradeoff of each

My recommendation: offline gate for prompt templates, system prompts, and fixed RAG scaffolds; sidecar for continuous evidence; inline only for a small, high-value predicate where the latency is affordable (a tool-argument validator, say, doesn't need 200 draws because it's not statistical).

Engineering overhead beyond latency: specs, boundaries, and version drift

Latency is honestly the easy part, because you can measure it. What kills projects is ongoing ownership.

Specifying the property is the hard part, and the spec is code you now have to maintain

"Is this advice safe?" can't be written as a predicate. "The response contains no dose recommendation above X for a patient with condition Y" can. The distance between those two sentences is where most certification projects die, and it's a policy problem no verifier solves.

Once you write the spec, it's code: versioned, reviewed, tested, subject to the same drift as everything else. A spec bug is now a soundness bug in your safety claim. Budget for it.

Modeling the surrounding pipeline: retrieval, prompt assembly, post-filtering — the verified boundary is usually smaller than the product

Your verified artifact is a model plus a prompt template. Your product is retrieval, reranking, template assembly, the model, output parsing, a post-filter, and a tool dispatcher. The certified boundary covers maybe 30% of the bytes the user actually sees.

A certificate about the model says nothing about the retrieved document that carried an instruction, the template that concatenated it without a delimiter, or the post-filter that stripped a refusal because it looked like a formatting error. Draw the boundary explicitly, in the same doc as the certificate, and name what's outside it.

Version drift: every weight, tokenizer, or kernel change invalidates the certificate

This is the sharpest one. A certificate is a claim about a specific function. Change the weights, the tokenizer, the prompt template, the CUDA kernel, the framework version, or the quantization scheme and you have a different function. The certificate doesn't transfer. It doesn't degrade gracefully either — it becomes meaningless while looking valid.

Practical mitigation: bind the certificate to a hash of everything that determines the function, and make the certificate unreadable if the hash doesn't match. A JSON artifact with model_sha, tokenizer_sha, template_sha, torch_version, cublas_version, precision fields, plus a CI job that regenerates the hash on every build. Then "is this certified?" is a hash comparison, not a trust exercise.

The CI shape — what a re-certification job looks like and what it gates

name: recertify
on:
  push:
    paths:
      - "models/lockfile.json"
      - "prompts/**"
      - "specs/**"
      - "requirements.txt"
jobs:
  certify:
    runs-on: gpu-a10g
    steps:
      - uses: actions/checkout@v4
      - run: python certify.py --spec specs/refusal.prompt.yaml
               --seeds 0,1,2 --n 200 --alpha 1e-3 --out artifacts/cert.json
      - run: python gate.py --current artifacts/cert.json
               --baseline artifacts/cert.baseline.json --min-lower 0.94

Two design notes from having run things like this. Use multiple seeds and gate on the worst one — a single seed hides seed-sensitivity, and seed-sensitivity is real when your draw distribution is small. Gate on the lower bound, never the point estimate, or you'll ship a build whose 0.949 became 0.941 and see a green check.

Failure modes that a provable inference guarantee does not catch

The section I'd want a reader to remember.

The specification gap: a certified property that is not the property you care about

Certification is very good at proving the thing you wrote down. It has no opinion on whether that's the thing you meant. A system that certifiably conforms to a schema and certifiably refuses on a keyword list can be perfectly certified and perfectly unhelpful — or harmful — in ways the spec never mentioned. That gap is the largest single risk in any certification program, and it's not a technical problem.

Distribution shift outside the perturbation set — the certificate says nothing about inputs it never quantified over

A radius certificate is a statement about a ball. Inputs outside the ball are unconstrained. In deployment, real traffic drifts outside the covered set within weeks and nothing in the certificate notices. This is exactly the gap monitoring fills, which is why certification and monitoring complement each other rather than substitute.

Prompt injection as an effectively unbounded input space, and why a radius does not cover it

Injection is the clearest illustration of why the metric matters. The input space an attacker can reach through injection isn't a ball around a benign prompt — it's roughly "any text a third party can get into the context window". An L2 radius of 0.1 in embedding space covers a set that's simultaneously too small (misses obvious semantic variants) and too large (includes incoherent inputs nobody sends).

There's real work on certifying safety against adversarial suffixes, and its honest claim is narrow: certificates hold over a defined set of suffix perturbations under a specific threat model. Useful for hardening that surface. Not a defense against injection in general — and neither is a smaller radius in a metric you chose because it was tractable.

Side effects outside the verified boundary: tool calls, retrieval writes, downstream services

Your model produced a certified token sequence. Then the agent runtime parsed it, called delete_record, and wrote to a vector store. Nothing in the certificate covered the dispatcher, the tool's authorization check, or the idempotency of the write. Verified inference plus an unverified actuator is not a verified system; it's a verified component with an unverified blast radius.

Sampling and non-determinism: what a guarantee means when temperature is above zero

A certificate about argmax tells you nothing about a system running temperature=0.8, top_p=0.95. Under sampling the object you can certify is a distributional property — say, that the refusal probability exceeds a threshold — and that requires reasoning about two sources of randomness: input perturbation and decoding sample.

Randomized smoothing handles the first, not the second. A certificate covering both would need to bound the sampling distribution itself, which is much harder and, as far as I know, not something production systems currently do. The honest engineering answer: run certification against the decoding configuration you actually deploy, and if it's greedy, say so in the certificate. A greedy-only certificate attached to a sampled endpoint is a mislabeled artifact.

Semantic properties that resist formalization ("is this advice safe", "is this citation real")

"Is this citation real" is checkable against a citation index — retrieval, not verification, and cheaper and more reliable than certification. "Is this advice safe" is a policy judgement that varies by user, jurisdiction, and context. No verifier will formalize it.

The line is pretty consistent: properties that reduce to syntax, schemas, ranges, and reference lookups are certifiable today and worth the cost. Properties that require world knowledge or normative judgement are not, and spending a quarter trying to formalize them is how a certification program loses its budget.

Where provable inference fits alongside evals, guardrails, and monitoring

The question I get most often is whether certification replaces the existing stack. It doesn't, and treating it as a replacement is the fastest way to make it useless.

Evals measure average behaviour, guardrails block known patterns, monitoring catches drift — certification bounds a neighborhood

No layer in that table answers "is this input outside the set and also harmful". That's the gap that remains after you've bought all four, and it's why input-side defense-in-depth (retrieval provenance, tool authorization, output-side policy checks) stays necessary.

Which layer answers which question, and the questions none of them answer

In plain terms, the questions none of them answer:

• Is this input one an attacker can actually construct?
• Is the property we certified the property the business cares about?
• Did the tool call that followed the certified output do something safe?
• Is the retrieved document trustworthy?

Certification buys you one specific, narrow, valuable thing: a universally quantified statement about a set you defined. Everything else still has to be built.

Defensive recommendations for teams evaluating provable inference today

Start with a property you can already test, then ask whether it is formalizable

Take an assertion that already lives in your test suite — "never emits a dose above X", "always returns valid JSON with these three fields", "never calls a destructive tool without a confirmation token". That's your candidate. If it reduces to a schema, a range, or an automaton, you can certify it this quarter with a grammar constraint or a bounded check. If it requires judgement, stop and harden the surrounding pipeline instead.

Budget the latency before promising the guarantee, and measure it on your own hardware

Run max_batch against your production model before you write the design doc. The ratio n / batching_speedup is roughly your capacity multiplier, and it's the number the platform team will ask about. If it's 150x, you're not doing this inline. Choose the offline gate and say so up front instead of discovering it during rollout.

And pick n from the bound you need, not a round number. My harness shows the bound going 0.875 → 0.949 → 0.983 as n goes 50 → 200 → 1000. Take the smallest n that clears your gate.

Treat certification as a narrow, expiring claim in your risk register, not a safety certificate

Write it as: "on model build sha, under perturbation set P, property Q held with CP lower bound p at alpha, as of date." With an expiry. With a re-certification trigger tied to the model hash. Never as "the system is provably safe", which shouldn't appear in any document.

Conclusion: a narrower claim, honestly scoped, is worth more than a broad one nobody can verify

Anthropic publishing on provable inference for LLMs is a genuinely interesting signal — formal methods moving from image classifiers toward the systems people actually deploy. But the announcement I can see is a title and a date. I don't know which models were verified, which property was certified, what perturbation set was used, or what it cost. Those four items are the difference between a result and a press release, and any engineer evaluating the work should ask for them in that order.

The position I'll defend: for LLM systems in production today, "provable" is useful in a narrow, output-shaped form. A certificate that a decoded response conforms to a grammar, stays within argument ranges, and fires a refusal predicate over an explicitly enumerated input set is achievable, cheap to run in CI, and honest about its boundaries. A certified robustness radius in a metric nobody's attacker is constrained by is a research result wearing production clothes.

The math doesn't care which one you pick. It will prove exactly the smaller claim you wrote down, including all the parts you forgot to exclude — which is why the "not claimed" line in the report is the most important line in it.

Further Reading

• News index entry: "Progress on provable inference for large language models" (Anthropic, 2026-11-03) — the primary source referenced in this post; the announcement summary only, not the full technical content.
• Cohen, Rosenfeld, Kolter — Certified Adversarial Robustness via Randomized Smoothing (arXiv:1902.02918) — the paper behind the radius/sample-size tradeoff discussed above.
• Katz et al. — Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (arXiv:1711.00851) — the completeness/branching blowup in its original form.
• Gowal et al. — Scalable Verified Training for Provably Robust Image Classification (arXiv:1902.04615) — interval bound propagation at scale, and where its bounds go vacuous.
• Kumar et al. — Certifying LLM Safety against Adversarial Prompting (arXiv:2404.00820) — the narrow suffix-perturbation threat model referenced in the injection section.
• OWASP Top 10 for LLM Applications — the surrounding-risk checklist that certification does not replace, particularly around excessive agency and tool use.