license: apache-2.0
task_categories:

• other
  tags:
• verification
• adversarial
• formal-methods
• eda
• certificates
• benchmark
• red-teaming
  pretty_name: Certificate Failure Atlas
  size_categories:
• n<1K
  configs:
• config_name: default
  data_files:
  • split: valid
    path: data/valid-*.jsonl
  • split: invalid
    path: data/invalid-*.jsonl

dataset_info:
features:
- name: id
dtype: string
- name: family
dtype: string
- name: valid
dtype: bool
- name: defect
dtype: string
- name: severity
dtype: string
- name: title
dtype: string
- name: why_it_looks_valid
dtype: string
- name: caught_by
dtype: string
- name: tags
sequence: string
- name: artifact_files
sequence: string
- name: artifact_json
dtype: string
- name: atlas_version
dtype: string
- name: atlas_digest
dtype: string
splits:
- name: valid
num_examples: 8
- name: invalid
num_examples: 28

Certificate Failure Atlas

A labelled corpus of proof-carrying artifacts that look valid and are not, with a two-sided
metric for scoring any verifier against them.

Why this exists

Verifiers are almost always tested on artifacts they are supposed to accept. What matters is what
they reject, and there was no public corpus of near-miss forgeries to test that against. So a
verifier's soundness was usually an assertion by its own author.

Every case here is a real artifact produced by a real toolchain, then mutated in one specific,
named way — with the defect label, why the forgery looks valid, and which check is supposed to
catch it.

Usage

from datasets import load_dataset

ds = load_dataset("nickh007/cert-atlas")
row = ds["invalid"][0]
print(row["id"], "|", row["severity"])
print(row["why_it_looks_valid"])
print(row["caught_by"])

No datasets install? The corpus is small and the loader is dependency-free:

from loader import load, iter_forgeries
d = load()                       # {"valid": [...], "invalid": [...]}
for case in iter_forgeries():
    print(case["id"], case["title"])

To actually score a verifier, use the generator package rather than the flat rows — artifacts
are directories and file groups that a table cannot fully represent:

pip install "cert-atlas @ git+https://github.com/nickharris808/cert-atlas.git@main"
cert-atlas build atlas
cert-atlas score atlas -- my-verifier --check '{path}'

Not on PyPI yet. The name cert-atlas is unregistered, so pip install cert-atlas installs
nothing today — use the line above, which installs exactly the same code.

Schema

artifact_json is a JSON object mapping each filename to its contents, so a single row
reconstructs the whole artifact — a bundle.json plus its payload files, a receipt, or a sealed
specification. It is a string rather than a nested mapping because filenames differ per case, and a
struct over the union of every filename defeats columnar schema inference.

import json
artifact = json.loads(row["artifact_json"])      # {"bundle.json": "...", ...}

Fields that only apply to forgeries (defect, severity, title, why_it_looks_valid,
caught_by) are the empty string on valid rows, not null, so every column has one stable type.

Splits

Families: certificate, receipt, seal, sequential.

By family: certificate (1 valid / 11 forged), receipt (2 / 8), sequential (3 / 6), seal (2 / 3) — 8 valid and 28 forged in total.

The metric

detection   = invalid artifacts correctly REJECTED / all invalid
precision   = valid   artifacts correctly ACCEPTED / all valid
atlas_score = min(detection, precision)

Ranking on the minimum is the design. Measured:

Both degenerate controls ship with the tooling. Run them before you trust any number on this
page — a benchmark on which doing nothing scores well is measuring nothing:

cert-atlas build atlas
cert-atlas baseline atlas          # reference verifier, artifact-only track

The two controls are cert_atlas.reference.accept_everything and reject_everything; scoring either
gives atlas_score 0.0000, from opposite sides. The scorer prints the digest with every run, so a
score is only comparable to the table above when the digest matches the one under Provenance.

Scoring needs only the Python standard library — not the three producer packages, which are
needed to build the corpus and nothing else. That separation was broken in releases before
cert-atlas 1.1.0 and is now enforced by a test that makes the interpreter answer rather than by a
promise; see docs/STRANGER.md.

Three cases worth reading

• receipt.swapped_cnf — the proof genuinely refutes the formula presented; it just is not the
  formula corresponding to the circuits. Catching it needs the encoder identity committed, not
  only the proof.
• cert.vacuous — every certificate deleted. The bundle stays well-formed, so a pure format
  check reports success. This case exists because it was found by attacking the reference verifier,
  which had the bug.
• seal.repointed_bound_seal — criteria doctored and a matching seal minted, so the two agree
  perfectly with each other. Only a binding over both catches it.

Provenance

Generated by cert-atlas 1.1.0 (atlas format version 1.0.0; the corpus is unchanged since
1.0.0 and the digest below is the same) from artifacts produced by the
reference toolchain (lcert-verify, equiv-receipt, prereg-seal), then mutated by the named
transformations in cert_atlas.generate. No third-party or proprietary data is included; every
artifact is synthetic and generated on demand.

Atlas digest: f278ae0d7fe885623b1b1ad2c3a742591a55d3c04bef6135b8e254d64e0abf64

The corpus is byte-reproducible — nothing is randomised, and cert-atlas build from a fixed
version yields this digest. Results at different digests are not comparable, and the scorer reports
the digest with every run.

Limitations

• Hand-designed, not exhaustive. Scoring 1.000 means sound against these 28 forgeries — a lower
  bound on soundness, never a proof of it.
• Cases are deliberately small; they exercise decision logic rather than scale.
• The forgeries were written by the same authors as the reference verifier. That is a real bias, and
  it is why adversarial contributions matter more than passing scores.
• The corpus tests verifiers, not physics. It says nothing about whether a certificate's numbers
  describe a real physical object.

The rest of the toolkit

Licence

Apache-2.0. See LICENSE.