diff --git a/Justfile b/Justfile
index 288830e9..9b0f128f 100644
--- a/Justfile
+++ b/Justfile
@@ -713,3 +713,17 @@ uncloak:
     else
         echo "Use 'ls -a' to view dotfiles on this OS."
     fi
+
+# ── mathesis: estate maths catalogue ──────────────────────────────────────
+
+# Re-run the proof census over docs/catalogue/census/repos.jsonl and regenerate the catalogue
+census:
+    bash scripts/census/run-census.sh
+
+# Re-render docs/catalogue/catalogue.adoc from the committed census rows
+catalogue:
+    bash scripts/census/render-catalogue.sh docs/catalogue/census > docs/catalogue/catalogue.adoc
+
+# Fail if the committed catalogue does not match the committed census rows
+catalogue-check:
+    bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -
diff --git a/README.adoc b/README.adoc
index bb804a44..f8cbdc03 100644
--- a/README.adoc
+++ b/README.adoc
@@ -1,172 +1,85 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath)
-= {{PROJECT_NAME}}
+= mathesis
 :toc:
-:toc-placement: preamble
 
-// ── Licensing ───────────────────────────────────────────────────────────────
-image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code licence: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"]
-image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"]
-image:https://img.shields.io/badge/Provenance-Quantum--Safe-blueviolet[Quantum-Safe Provenance,link="docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt"]
+The estate's maths section. It answers "where does that proof live?" for
+every hyperpolymath repository: which repos carry proofs, in which prover,
+whether the work reads as theory or engineering, which have holes or
+axioms, and where each repo's proof-status file is.
 
-// ── Standard & quality gates ────────────────────────────────────────────────
-image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"]
-image:https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/{{OWNER}}/{{REPO}}/governance-badges/badges/k9.json[K9 conformance,link="https://github.com/{{OWNER}}/{{REPO}}/actions/workflows/dogfood-gate.yml"]
-image:https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}/badge[OpenSSF Best Practices,link="https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}"]
-image:https://api.scorecard.dev/projects/github.com/{{OWNER}}/{{REPO}}/badge[OpenSSF Scorecard,link="https://scorecard.dev/viewer/?uri=github.com/{{OWNER}}/{{REPO}}"]
-image:https://sonarcloud.io/api/project_badges/measure?project={{OWNER}}_{{REPO}}&metric=alert_status[SonarQube Quality Gate,link="https://sonarcloud.io/summary/new_code?id={{OWNER}}_{{REPO}}"]
-image:https://archive.softwareheritage.org/badge/origin/https://{{FORGE}}/{{OWNER}}/{{REPO}}/[Archived in Software Heritage,link="https://archive.softwareheritage.org/browse/origin/?origin_url=https://{{FORGE}}/{{OWNER}}/{{REPO}}"]
+Proofs stay in their home repositories. mathesis points at them. Later it
+will also hold the Agda sources for theory that has no other natural home.
 
-// ── Provenance & ecosystem ──────────────────────────────────────────────────
-image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"]
-image:https://img.shields.io/badge/Zig-Zero--overhead-F7A41D?logo=zig&logoColor=black[Zig Zero-overhead FFI,link="https://github.com/hyperpolymath/typed-wasm"]
-image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url={{FORGE}}"]
+The rules for where a proof *should* live are not here: they are
+`standards/3-practice/PROOF-POLICY.adoc` (Creusot for Rust, SPARK for Ada,
+Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked
+in Rocq and Lean). The working method is the proof-craft skill.
 
-{{PROJECT_DESCRIPTION}}
-
-[IMPORTANT]
-====
-*This file is a template.* You are reading `README.adoc` from the *RSR template repo*
-(or a freshly-cloned copy of it). Run `just repo-init` to replace every `{{PLACEHOLDER}}`
-token with your project's details, then delete this admonition. Until you do, the
-`{{...}}` markers below are intentional placeholders, not content.
-====
-
-== What this is
-
-A new repository scaffolded from the *Rhodium Standard Repository (RSR)* template:
-a batteries-included starting point that ships with CI/CD, machine-readable project
-metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam
-(Idris2 + Zig), container and reproducible-build scaffolding, and governance
-infrastructure — all wired and passing the RSR validators on day one.
-
-Replace this section with a description of *your* project once initialised.
-
-== Quick start
-
-[source,bash]
-----
-# 1. Create a repo from this template (or clone it), then from the repo root:
-just repo-init                # interactive bootstrap: fills every {{PLACEHOLDER}}
-
-# 2. See the available tasks:
-just                     # lists all phases (build, test, validate, audit, ...)
-
-# 3. Check the repo still satisfies the RSR shape:
-just validate            # structure + metadata checks
-----
-
-`just repo-init` prompts for the project name, owner, author, licence contact, and the
-other values listed in `.machine_readable/ai/PLACEHOLDERS.adoc`, substitutes them
-across the tree, validates the result, and (if available) runs the `k9-svc` checks.
-
-[[ai-install]]
-== AI-Assisted Installation (Recommended)
-
-=== Just say it
-
-Say this to any AI assistant that can read a URL and run commands (or give you
-commands to paste):
-
-[source,text]
-----
-Create a new repository from https://github.com/hyperpolymath/rsr-template-repo
-----
-
-The URL is the key: it leads the assistant to
-link:docs/AI_INSTALLATION_GUIDE.adoc[`docs/AI_INSTALLATION_GUIDE.adoc`], the
-complete step-by-step recipe. The assistant checks your system, installs the
-prerequisites, instantiates the template with `just repo-init`, and verifies the
-result with `just doctor`.
-
-* "Set up rsr-template-repo so I can work on the template itself — https://github.com/hyperpolymath/rsr-template-repo"
-* `./launcher.sh --ai-setup` (or `just ai-setup`) prints the line and the guide path.
-
-=== What you will be asked
-
-. Your operating system (Linux, macOS, or Windows via WSL2).
-. The new project's name, owner, author and licence contact (the values listed in
-  `.machine_readable/ai/PLACEHOLDERS.adoc`).
-. To confirm the privacy notice below.
-
-=== Privacy and security
-
-[IMPORTANT]
-====
-Setting up rsr-template-repo clones this repository and installs its developer
-tools per-user with mise (no administrator rights, nothing sent anywhere).
-`just repo-init` rewrites files only inside the new checkout; it creates no
-remote repository and pushes nothing until you do.
-====
-
-=== Minting without a terminal
-
-Agents and CI can mint non-interactively: set `RSR_NON_INTERACTIVE=1` and pass
-the answers as environment variables named like the prompts' variables in
-`build/just/repo-init.just` (`PROJECT_NAME`, `REPO`, `OWNER`, `AUTHOR` and
-`AUTHOR_EMAIL` are required; any other answer left unset is blank or takes its
-default). Piping the answers to stdin in prompt order also works.
-
-=== Troubleshooting
-
-Run `just doctor`; each FAIL carries a code explained in
-link:docs/SETUP.adoc#troubleshooting[`docs/SETUP.adoc` §Troubleshooting], and
-`just heal` applies the automatic fixes. Prefer to do it yourself? The full
-manual route is link:docs/SETUP.adoc[`docs/SETUP.adoc`]; developers and
-maintainers can brief an AI with `just ai-warmup dev` / `just ai-warmup maintainer`.
-
-== What you get
-
-* *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`,
-  `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`,
-  in deed, so tools and agents can read the project's state and boundaries.
-* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the
-  universal entry point that tells an AI agent how to work in this repo before it
-  touches anything; it carries the AI allocation policy and the ply directory tree.
-* *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over
-  `src/interface/ffi/` (Zig implementation), with generated C headers.
-* *CI/CD* — GitHub Actions for quality, security (CodeQL, Scorecard, secret
-  scanning), multi-forge mirroring, and RSR anti-pattern enforcement.
-* *Supply-chain & reproducibility* — container layering (stapeln), Guix shells,
-  SBOM, and signing hooks.
-* *Governance* — `GOVERNANCE.adoc`, `MAINTAINERS.adoc`, `.github/` community health
-  files, and a release `AUDIT.adoc` gate.
-
-== Repository map
-
-The authoritative map is generated, so it cannot drift from the tree:
-link:docs/architecture/REPOSITORY-MAP.adoc[docs/architecture/REPOSITORY-MAP.adoc]
-(regenerate with `just repo-map`; CI fails if it is stale).
-
-The short version:
+== What is here
 
 [cols="1,3"]
 |===
-| Path | What lives there
-
-| `README.adoc`, `CLAUDE.md` | Start here - humans and AI agents respectively.
-| `src/`, `tests/`           | The code and its tests.
-| `docs/`                    | Human documentation, including the full map above.
-| `.machine_readable/`        | Manifests, contractiles and policies that tools read.
-| `build/`, `Justfile`       | Every task runs through `just`; phases live in `build/just/`.
-| `ci/`, `.github/`          | CI configuration; GitHub reads `.github/` and no other path.
+|`docs/catalogue/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand.
+|`docs/catalogue/census/` |What the catalogue is rendered from: `catalogue-rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl` and `template-paths.txt`. Each JSONL file is I-JSON/JCS, one object per line.
+|`scripts/census/` |`run-census.sh` (whole census), `census-repo.sh` (one repo), `summarise.sh`, `build-rows.sh` (raw census to rows), `render-catalogue.sh` (rows to catalogue), and proof-craft's `proof-holes.sh`.
+|`Justfile` |`just census`, `just catalogue`, `just catalogue-check` (the committed catalogue matches the committed data).
 |===
 
-== Where to go next
-
-* link:docs/architecture/REPOSITORY-MAP.adoc[The repository map] — generated; what every directory is for.
-* link:docs/EXPLAINME.adoc[EXPLAINME] — the engineering deep-dive: how the pieces actually work.
-* link:docs/AFFIRMATION.adoc[AFFIRMATION] — the dated, signed honesty snapshot of the repo's true state.
-* link:docs/AUDIT.adoc[AUDIT] — the release audit gate.
-* link:docs/AI_INSTALLATION_GUIDE.adoc[AI installation guide] — for agents instantiating this template.
-* link:.machine_readable/ai/PLACEHOLDERS.adoc[PLACEHOLDERS] — the full placeholder reference.
+== How the census works
+
+. *List repositories.* `docs/catalogue/census/repos.jsonl` is the input. Agent sessions build
+  it with the Claude Code remote `list_repos` tool, because the GitHub API is
+  not reachable from them.
+. *List proof files cheaply.* Each repository is cloned blobless with
+  `--no-checkout`, and its file names are filtered by prover extension:
+  Agda, Idris2, Lean, Rocq, Isabelle, TLA+, Dedukti/Lambdapi, SMT-LIB, TPTP,
+  SPARK, Why3, F*, Dafny and Alloy.
+. *Read only the proof files.* Only those files are checked out. Top-level
+  declaration names go to `decls.jsonl`, and proof-craft's `proof-holes.sh`
+  inventories holes, axioms, disabled checkers and policy breaches
+  (`holes.jsonl`).
+. *Set the template aside.* Files the RSR template ships
+  (`docs/catalogue/census/template-paths.txt`) are boilerplate wherever they appear. The
+  catalogue counts only a repo's *own* files.
+. *Keep rows, not paths.* The raw, path-level census (clones, every proof file, every declaration, every hole finding, and a `summary.md`) goes to a scratch directory (`MATHESIS_WORK`) and is not committed. `build-rows.sh` folds it into one row of counts per repository, and only those rows are committed, so the data stays small and does not repeat other repositories' file paths.
+
+== Reading the catalogue (first pass, 2026-10-26)
+
+The first census covered 476 repositories:
+
+* *Scope:* 462 repositories were cloned; 5 forks and 9 awesome-lists were
+  skipped. 275 have proof files, and 239 still have them once template
+  boilerplate is set aside.
+* *Unreached:* 37 private repositories could not be cloned and are listed at
+  the end of the catalogue, among them `cut-calculus`.
+* *Possibly missing:* the listing returned only repositories pushed since
+  2026-09-15, so older, untouched repos may be absent. Add them to
+  `docs/catalogue/census/repos.jsonl` and rerun.
+* *Theory or engineering* is a heuristic: more Agda, Lean, Rocq or Isabelle
+  files than Idris2 or SPARK files reads as theory. Confirm each row against
+  PROOF-POLICY.
+* *Hole, axiom, unsafe and policy counts* are textual candidates, not kernel
+  verdicts. The kernel is the authority. `import Mathlib` shows under
+  policy.
+* *Declaration counts* overcount Agda and Idris2:
+  every column-0 type signature counts, helpers included.
+* *Older template copies* survive as "own" files in some repos: for example
+  asdf-tool-plugins, whose plugins each carry a stubbed `Layout.idr`.
+* *Fixtures:* files under `tests/`, `fixtures/`, `corpus/` or `benches/` are
+  counted as fixtures. `examples/` is not, because some verifiers (Atoma)
+  keep real verification conditions there.
+
+== Next steps
+
+* Confirm the theory/engineering split per row, and record each repo's
+  obligations with the status vocabulary of PROOF-POLICY §5.
+* Theorem-level rows for the theory repos: statement, Agda source, Rocq
+  leg, Lean leg, route.
+* A scheduled CI job that reruns the census and fails on catalogue drift.
+* A deed (`mathesis_chora.deed`) once the repo is instantiated from the RSR
+  template.
 
 == Licence
 
-Code, configuration and scripts are link:LICENSE[Mozilla Public License 2.0]
-(`MPL-2.0`); prose documentation is `CC-BY-SA-4.0`. Both texts live in
-`LICENSES/`, and per-file `SPDX-License-Identifier` headers are authoritative.
-The GitHub-detected licence is MPL-2.0 (the root `LICENSE`). Long-term
-attribution uses Quantum-Safe Provenance — see
-link:docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt[the Quantum-Safe Provenance exhibit].
+Code (`scripts/`, `Justfile`): MPL-2.0. Documentation and the catalogue:
+CC-BY-SA-4.0. See `LICENSES/`.
diff --git a/docs/catalogue/catalogue.adoc b/docs/catalogue/catalogue.adoc
new file mode 100644
index 00000000..7b1903be
--- /dev/null
+++ b/docs/catalogue/catalogue.adoc
@@ -0,0 +1,550 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Estate maths catalogue
+:toc:
+
+Generated by `scripts/census/render-catalogue.sh` from the census of
+476 repositories. Do not edit by hand; rerun the census.
+
+Each row is a repository with proof files of its own, after the files the RSR
+template ships as boilerplate are set aside. *Theory* and *engineering* are a
+first-pass sort (more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK files
+reads as theory); confirm each row against PROOF-POLICY before relying on it.
+Declarations are top-level names found by keyword and signature rules, so
+Agda and Idris2 counts include helpers. Hole, axiom, unsafe and policy counts
+come from proof-craft's `proof-holes.sh`: textual candidates, not kernel
+verdicts.
+
+== Theory
+
+[cols="3,1,1,4,1,1,1,1,1,3",options="header"]
+|===
+|Repository |Own files |Fixtures |Provers (files) |Declarations |Holes |Axioms |Unsafe |Policy |Proof-status doc
+
+|https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] |148 |0 |agda 148 |1467 |0 |1 |0 |1 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/valence-shell[hyperpolymath/valence-shell] |64 |0 |agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5 |960 |5 |1 |0 |9 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/affinescript[hyperpolymath/affinescript] |54 |0 |agda 23, lean 1, rocq 21, idris2 9 |568 |9 |1 |0 |0 |`docs/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/gnpl[hyperpolymath/gnpl] |53 |8 |lean 49, idris2 4 |737 |5 |7 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/protocol-squisher[hyperpolymath/protocol-squisher] |42 |0 |agda 10, lean 4, rocq 4, isabelle 2, idris2 12, tla 6, smt-atp 4 |365 |2 |2 |0 |0 |`provenance/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/absolute-zero[hyperpolymath/absolute-zero] |40 |0 |agda 5, lean 11, rocq 16, isabelle 2, idris2 5, smt-atp 1 |950 |7 |89 |0 |4 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/firmboot[hyperpolymath/firmboot] |38 |0 |agda 19, lean 19 |409 |0 |1 |0 |0 |—
+
+|https://github.com/hyperpolymath/epistemic-types[hyperpolymath/epistemic-types] |37 |14 |agda 37 |320 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/trope-checker[hyperpolymath/trope-checker] |37 |0 |agda 10, lean 11, idris2 16 |492 |10 |0 |0 |1 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/arghda-core[hyperpolymath/arghda-core] |32 |32 |agda 13, lean 2, rocq 4, isabelle 4, idris2 7, smt-atp 2 |15 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/tropical-types[hyperpolymath/tropical-types] |28 |0 |lean 19, isabelle 9 |540 |5 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/residual-evidence-types[hyperpolymath/residual-evidence-types] |27 |13 |agda 27 |328 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/choreographic-types[hyperpolymath/choreographic-types] |25 |6 |agda 25 |178 |0 |1 |0 |1 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/my-lang[hyperpolymath/my-lang] |25 |0 |rocq 16, idris2 9 |617 |0 |26 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/resource-algebra[hyperpolymath/resource-algebra] |22 |12 |agda 22 |271 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/atoma[hyperpolymath/atoma] |21 |0 |agda 4, idris2 3, smt-atp 14 |127 |0 |0 |0 |4 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/system-et[hyperpolymath/system-et] |21 |0 |lean 21 |164 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/occupancy-types[hyperpolymath/occupancy-types] |19 |2 |agda 8, lean 5, idris2 6 |76 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/wokelang[hyperpolymath/wokelang] |18 |0 |lean 7, rocq 3, idris2 8 |418 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/JuliaPackageSpitter.jl[hyperpolymath/JuliaPackageSpitter.jl] |17 |12 |agda 17 |83 |1 |1 |1 |1 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/secret-types[hyperpolymath/secret-types] |16 |3 |agda 16 |67 |0 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/hyperpolymath/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |1 |0 |6 |`proofs/PROOF-STATUS.md`
+
+|https://github.com/hyperpolymath/marches[hyperpolymath/marches] |15 |0 |lean 15 |161 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/zotero-tools[hyperpolymath/zotero-tools] |15 |0 |lean 9, idris2 3, tla 3 |94 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/lithoglyph[hyperpolymath/lithoglyph] |13 |0 |lean 8, idris2 5 |264 |1 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/MetaManifold-Evidence[metadatastician/MetaManifold-Evidence] |13 |0 |agda 13 |70 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/phronesis[hyperpolymath/phronesis] |12 |0 |agda 3, lean 3, rocq 1, idris2 2, tla 3 |140 |3 |0 |0 |2 |—
+
+|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |11 |0 |agda 11 |51 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`
+
+|https://github.com/hyperpolymath/eclexia[hyperpolymath/eclexia] |11 |0 |agda 1, rocq 6, idris2 4 |218 |0 |5 |0 |1 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/CompositionalCounts.jl[hyperpolymath/CompositionalCounts.jl] |10 |0 |agda 10 |184 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/jtv-lang[hyperpolymath/jtv-lang] |10 |0 |lean 9, idris2 1 |225 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/ExactTests.jl[hyperpolymath/ExactTests.jl] |9 |0 |agda 9 |44 |0 |1 |0 |1 |—
+
+|https://github.com/metadatastician/hvn-dehallucinator[metadatastician/hvn-dehallucinator] |9 |3 |agda 5, idris2 1, tla 3 |108 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/boinc-boinc[hyperpolymath/boinc-boinc] |8 |0 |lean 8 |46 |1 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/echidnabot[hyperpolymath/echidnabot] |7 |0 |lean 2, rocq 2, idris2 3 |63 |6 |0 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/gitbot-fleet[hyperpolymath/gitbot-fleet] |7 |0 |lean 2, rocq 2, idris2 3 |63 |6 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/kitchenspeak[hyperpolymath/kitchenspeak] |6 |0 |agda 5, idris2 1 |82 |0 |4 |0 |1 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/neurophone[hyperpolymath/neurophone] |6 |0 |lean 3, tla 2, dafny 1 |19 |0 |0 |0 |6 |—
+
+|https://github.com/metadatastician/lintel[metadatastician/lintel] |6 |4 |agda 6 |58 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/palimpsest-license[hyperpolymath/palimpsest-license] |5 |4 |agda 5 |3 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/autoformal-fidelity[hyperpolymath/autoformal-fidelity] |4 |1 |agda 4 |7 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/statistikles[hyperpolymath/statistikles] |4 |0 |agda 4 |22 |0 |0 |0 |3 |`PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/megadog[catachresis-colloquium/megadog] |3 |0 |lean 3 |25 |0 |0 |0 |3 |—
+
+|https://github.com/hyperpolymath/nextgen-typing[hyperpolymath/nextgen-typing] |3 |0 |agda 3 |16 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/snifs[hyperpolymath/snifs] |3 |0 |agda 2, idris2 1 |43 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/tangle[hyperpolymath/tangle] |3 |0 |lean 3 |61 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/ZenodoDeposits.jl[metadatastician/ZenodoDeposits.jl] |3 |0 |agda 3 |53 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ResidualEvidenceTypes.jl[hyperpolymath/ResidualEvidenceTypes.jl] |1 |1 |agda 1 |1 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/invariant-path[hyperpolymath/invariant-path] |1 |0 |agda 1 |8 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/zerostep[hyperpolymath/zerostep] |1 |0 |isabelle 1 |16 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+|===
+
+== Engineering (APIs, ABIs, code)
+
+[cols="3,1,1,4,1,1,1,1,1,3",options="header"]
+|===
+|Repository |Own files |Fixtures |Provers (files) |Declarations |Holes |Axioms |Unsafe |Policy |Proof-status doc
+
+|https://github.com/hyperpolymath/proven-servers[hyperpolymath/proven-servers] |1097 |0 |idris2 899, spark 197, other 1 |6242 |3 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/proven[hyperpolymath/proven] |967 |61 |lean 14, idris2 906, spark 42, tla 1, other 4 |11166 |22 |0 |10 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/developer-ecosystem[hyperpolymath/developer-ecosystem] |722 |41 |agda 2, lean 3, rocq 274, idris2 347, spark 91, tla 2, other 3 |4024 |91 |0 |61 |2 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/asdf-tool-plugins[hyperpolymath/asdf-tool-plugins] |567 |0 |idris2 567 |11340 |567 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/boj-server-cartridges[hyperpolymath/boj-server-cartridges] |184 |0 |idris2 184 |1500 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/echidna[hyperpolymath/echidna] |167 |21 |agda 24, lean 17, rocq 9, isabelle 6, idris2 49, spark 18, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4 |1885 |4 |1 |4 |23 |`docs/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ambientops[hyperpolymath/ambientops] |102 |1 |idris2 39, spark 58, other 5 |777 |39 |0 |8 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/cerro-torre[metadatastician/cerro-torre] |85 |1 |idris2 8, spark 75, other 2 |91 |18 |0 |69 |0 |—
+
+|https://github.com/hyperpolymath/proven-tests-and-benches[hyperpolymath/proven-tests-and-benches] |72 |27 |idris2 72 |857 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/trigger[hyperpolymath/trigger] |64 |20 |agda 2, idris2 5, spark 56, other 1 |165 |0 |13 |0 |0 |—
+
+|https://github.com/metadatastician/gossamer[metadatastician/gossamer] |62 |10 |idris2 53, tla 9 |1868 |0 |0 |8 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/metadatastician/paint-type[metadatastician/paint-type] |51 |8 |agda 2, lean 1, idris2 42, tla 6 |991 |4 |0 |8 |2 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ochrance[hyperpolymath/ochrance] |48 |8 |idris2 48 |404 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/typed-wasm[hyperpolymath/typed-wasm] |46 |12 |idris2 46 |850 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ephapax[hyperpolymath/ephapax] |43 |0 |rocq 19, idris2 24 |635 |15 |0 |1 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/hypatia[hyperpolymath/hypatia] |42 |11 |agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1 |448 |3 |1 |0 |1 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/vexometer[hyperpolymath/vexometer] |42 |6 |idris2 10, spark 29, other 3 |104 |3 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/bitfuckit[hyperpolymath/bitfuckit] |39 |0 |spark 37, other 2 |0 |0 |0 |2 |0 |—
+
+|https://github.com/hyperpolymath/contractiles[hyperpolymath/contractiles] |36 |0 |spark 34, other 2 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/vcl-ut[hyperpolymath/vcl-ut] |36 |15 |idris2 36 |953 |0 |0 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/metadatastician/_pathroot[metadatastician/_pathroot] |34 |0 |idris2 5, spark 25, other 4 |70 |3 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/resource-record-fluctuator[hyperpolymath/resource-record-fluctuator] |32 |0 |spark 31, other 1 |0 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/universal-modding-studio[catachresis-colloquium/universal-modding-studio] |29 |0 |idris2 25, spark 3, other 1 |254 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/boj-server[hyperpolymath/boj-server] |26 |0 |idris2 19, tla 6, alloy 1 |421 |4 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/julia-ecosystem[hyperpolymath/julia-ecosystem] |25 |0 |idris2 25 |399 |15 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/nextgen-databases[hyperpolymath/nextgen-databases] |24 |3 |idris2 24 |279 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ssg-collection[hyperpolymath/ssg-collection] |23 |0 |lean 1, idris2 6, spark 13, other 3 |108 |3 |0 |4 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/vordr[metadatastician/vordr] |23 |2 |idris2 10, spark 12, other 1 |122 |0 |0 |4 |0 |—
+
+|https://github.com/hyperpolymath/raze-tui[hyperpolymath/raze-tui] |22 |0 |idris2 3, spark 18, other 1 |59 |0 |0 |2 |0 |—
+
+|https://github.com/hyperpolymath/verisimdb[hyperpolymath/verisimdb] |20 |0 |rocq 9, idris2 11 |365 |3 |43 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/metadatastician/groove[metadatastician/groove] |19 |3 |idris2 19 |185 |0 |0 |0 |0 |—
+
+|https://github.com/metadatastician/stapeln[metadatastician/stapeln] |19 |8 |idris2 18, alloy 1 |294 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/deed-core[hyperpolymath/deed-core] |18 |0 |idris2 15, spark 3 |161 |0 |0 |10 |0 |—
+
+|https://github.com/hyperpolymath/iseriser[hyperpolymath/iseriser] |18 |0 |idris2 18 |254 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/lol[hyperpolymath/lol] |18 |0 |agda 3, idris2 15 |314 |0 |2 |0 |2 |`docs/proof-debt.md`
+
+|https://github.com/hyperpolymath/reposystem[hyperpolymath/reposystem] |16 |1 |idris2 1, spark 13, other 2 |7 |0 |0 |2 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/tree-navigator[hyperpolymath/tree-navigator] |16 |0 |spark 15, other 1 |0 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/anytype[hyperpolymath/anytype] |14 |1 |idris2 14 |80 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/betlang[hyperpolymath/betlang] |14 |9 |lean 3, idris2 11 |95 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/flatracoon[hyperpolymath/flatracoon] |14 |0 |idris2 3, spark 9, other 2 |47 |3 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/ochrance-framework[hyperpolymath/ochrance-framework] |14 |0 |idris2 14 |123 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/civic-connect[hyperpolymath/civic-connect] |13 |0 |idris2 4, spark 8, other 1 |46 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/docudactyl[hyperpolymath/docudactyl] |13 |0 |idris2 7, spark 5, other 1 |223 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/kategoria[hyperpolymath/kategoria] |13 |0 |idris2 13 |105 |1 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/robodog-defensive-systems-lab[hyperpolymath/robodog-defensive-systems-lab] |13 |0 |idris2 6, spark 6, other 1 |64 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/modshells[hyperpolymath/modshells] |12 |2 |spark 9, other 3 |0 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/panll[hyperpolymath/panll] |12 |6 |idris2 12 |125 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/universal-chat-extractor[hyperpolymath/universal-chat-extractor] |12 |9 |idris2 12 |110 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/verisimiser[hyperpolymath/verisimiser] |12 |0 |idris2 12 |208 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/zerotier-k8s-link[hyperpolymath/zerotier-k8s-link] |12 |8 |idris2 12 |110 |3 |0 |0 |0 |—
+
+|https://github.com/metadatastician/burble[metadatastician/burble] |12 |0 |idris2 12 |127 |0 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/metadatastician/cleave[metadatastician/cleave] |12 |3 |idris2 12 |38 |0 |0 |0 |0 |`docs/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/Axiom.jl[hyperpolymath/Axiom.jl] |11 |0 |idris2 11 |131 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/docmatrix[hyperpolymath/docmatrix] |11 |0 |spark 10, other 1 |0 |0 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/formatrix-docs[hyperpolymath/formatrix-docs] |11 |0 |spark 10, other 1 |0 |0 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/januskey[hyperpolymath/januskey] |11 |5 |agda 3, idris2 8 |142 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/polyglot-i18n[hyperpolymath/polyglot-i18n] |11 |0 |spark 10, other 1 |0 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/typedqliser[hyperpolymath/typedqliser] |11 |0 |idris2 11 |155 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/phi-LAM[metadatastician/phi-LAM] |11 |0 |lean 5, idris2 6 |199 |0 |4 |0 |0 |—
+
+|https://github.com/hyperpolymath/fireflag[hyperpolymath/fireflag] |10 |0 |idris2 10 |156 |0 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/thunderbird-template-reloaded[hyperpolymath/thunderbird-template-reloaded] |10 |9 |idris2 10 |74 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/IDApTIK[catachresis-colloquium/IDApTIK] |9 |0 |idris2 9 |120 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/affinescriptiser[hyperpolymath/affinescriptiser] |9 |0 |idris2 9 |147 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/alloyiser[hyperpolymath/alloyiser] |9 |0 |idris2 9 |139 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/anvomidaviser[hyperpolymath/anvomidaviser] |9 |0 |idris2 9 |140 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/atsiser[hyperpolymath/atsiser] |9 |0 |idris2 9 |137 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/betlangiser[hyperpolymath/betlangiser] |9 |0 |idris2 9 |173 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/bqniser[hyperpolymath/bqniser] |9 |0 |idris2 9 |132 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/chapeliser[hyperpolymath/chapeliser] |9 |0 |idris2 9 |136 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/dafniser[hyperpolymath/dafniser] |9 |0 |idris2 9 |146 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/eclexiaiser[hyperpolymath/eclexiaiser] |9 |0 |idris2 9 |121 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/ephapaxiser[hyperpolymath/ephapaxiser] |9 |0 |idris2 9 |133 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/futharkiser[hyperpolymath/futharkiser] |9 |0 |idris2 9 |136 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/halideiser[hyperpolymath/halideiser] |9 |0 |idris2 9 |161 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/idrisiser[hyperpolymath/idrisiser] |9 |0 |idris2 9 |122 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/julianiser[hyperpolymath/julianiser] |9 |0 |idris2 9 |140 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/lustreiser[hyperpolymath/lustreiser] |9 |0 |idris2 9 |141 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/maa-framework[hyperpolymath/maa-framework] |9 |2 |agda 3, spark 4, other 2 |11 |0 |0 |1 |2 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/mylangiser[hyperpolymath/mylangiser] |9 |0 |idris2 9 |135 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/nimiser[hyperpolymath/nimiser] |9 |0 |idris2 9 |147 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/oblibeniser[hyperpolymath/oblibeniser] |9 |0 |idris2 9 |156 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/oblibeny[hyperpolymath/oblibeny] |9 |0 |idris2 9 |99 |0 |0 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/otpiser[hyperpolymath/otpiser] |9 |0 |idris2 9 |157 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/phronesiser[hyperpolymath/phronesiser] |9 |0 |idris2 9 |155 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/ponyiser[hyperpolymath/ponyiser] |9 |0 |idris2 9 |137 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/tlaiser[hyperpolymath/tlaiser] |9 |0 |idris2 9 |181 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/wokelangiser[hyperpolymath/wokelangiser] |9 |0 |idris2 9 |143 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/0patch-lsa-sentinel[hyperpolymath/0patch-lsa-sentinel] |8 |0 |idris2 2, spark 5, other 1 |23 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/aerie[hyperpolymath/aerie] |8 |2 |idris2 8 |128 |1 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/deed-ecosystem[hyperpolymath/deed-ecosystem] |8 |3 |idris2 8 |99 |0 |0 |0 |0 |`deno/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/laniakea[hyperpolymath/laniakea] |8 |0 |idris2 7, alloy 1 |32 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/game-server-admin[catachresis-colloquium/game-server-admin] |7 |0 |idris2 7 |212 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/bofig[hyperpolymath/bofig] |7 |0 |idris2 7 |166 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/somethings-fishy[hyperpolymath/somethings-fishy] |7 |0 |spark 6, other 1 |0 |0 |0 |2 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ubicity[hyperpolymath/ubicity] |7 |6 |idris2 7 |76 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/veridical-simulation-core[hyperpolymath/veridical-simulation-core] |7 |0 |idris2 7 |51 |0 |0 |0 |0 |—
+
+|https://github.com/catachresis-colloquium/enaction-engine[catachresis-colloquium/enaction-engine] |6 |3 |idris2 6 |95 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/thejeffparadox[catachresis-colloquium/thejeffparadox] |6 |0 |spark 5, other 1 |0 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/conflow[hyperpolymath/conflow] |6 |0 |tla 6 |8 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/network-ambulance[hyperpolymath/network-ambulance] |6 |0 |spark 5, other 1 |0 |0 |0 |1 |0 |—
+
+|https://github.com/hyperpolymath/panic-attack[hyperpolymath/panic-attack] |6 |1 |idris2 6 |46 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/presswerk[hyperpolymath/presswerk] |6 |0 |idris2 6 |76 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/rpa-elysium[hyperpolymath/rpa-elysium] |6 |0 |idris2 6 |74 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/session-sentinel[hyperpolymath/session-sentinel] |6 |0 |idris2 6 |117 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/smtp-notify-action[hyperpolymath/smtp-notify-action] |6 |0 |idris2 6 |101 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/typell[hyperpolymath/typell] |6 |0 |idris2 6 |159 |3 |0 |0 |0 |`PROOF-STATUS.adoc`
+
+|https://github.com/metadatastician/insolvency-tycoon[metadatastician/insolvency-tycoon] |6 |0 |idris2 6 |25 |0 |0 |0 |0 |—
+
+|https://github.com/catachresis-colloquium/befunge93-vault-cracker[catachresis-colloquium/befunge93-vault-cracker] |5 |0 |idris2 5 |36 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/continuation-mesh[hyperpolymath/continuation-mesh] |5 |0 |idris2 5 |15 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/error-lang[hyperpolymath/error-lang] |5 |0 |idris2 5 |57 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/http-capability-gateway[hyperpolymath/http-capability-gateway] |5 |0 |idris2 5 |59 |1 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/hybrid-automation-router[hyperpolymath/hybrid-automation-router] |5 |0 |idris2 5 |66 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ipfs-overlay[hyperpolymath/ipfs-overlay] |5 |4 |idris2 5 |17 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/kaldor-iiot[hyperpolymath/kaldor-iiot] |5 |0 |idris2 5 |27 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/krl[hyperpolymath/krl] |5 |0 |agda 2, idris2 3 |61 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/quandledb[hyperpolymath/quandledb] |5 |0 |agda 1, idris2 1, tla 3 |36 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/evil-weevil[catachresis-colloquium/evil-weevil] |4 |0 |idris2 4 |124 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/pow-the-game[catachresis-colloquium/pow-the-game] |4 |0 |idris2 4 |14 |0 |0 |0 |0 |—
+
+|https://github.com/catachresis-colloquium/proof-of-work[catachresis-colloquium/proof-of-work] |4 |0 |idris2 4 |46 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/bebop-ffi[hyperpolymath/bebop-ffi] |4 |0 |idris2 4 |29 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/cloud-sync-tuner[hyperpolymath/cloud-sync-tuner] |4 |2 |spark 3, other 1 |0 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/conative-gating[hyperpolymath/conative-gating] |4 |0 |idris2 4 |23 |3 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/ddraig-ssg[hyperpolymath/ddraig-ssg] |4 |0 |idris2 4 |118 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/hpm-crypto-rsr[hyperpolymath/hpm-crypto-rsr] |4 |0 |idris2 4 |24 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/ideas-to-alphas[hyperpolymath/ideas-to-alphas] |4 |0 |idris2 4 |77 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/julia-professional-registry[hyperpolymath/julia-professional-registry] |4 |3 |idris2 4 |18 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/k9-ecosystem[hyperpolymath/k9-ecosystem] |4 |0 |idris2 4 |76 |0 |0 |0 |0 |`deno/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/odds-and-sods-package-manager[hyperpolymath/odds-and-sods-package-manager] |4 |0 |idris2 4 |41 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/patallm-gallery[hyperpolymath/patallm-gallery] |4 |0 |idris2 4 |113 |6 |0 |0 |0 |`PROOF-NEEDS.md`
+
+|https://github.com/hyperpolymath/quintessence[hyperpolymath/quintessence] |4 |0 |idris2 2, tla 2 |20 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/stateful-artefacts[hyperpolymath/stateful-artefacts] |4 |0 |idris2 2, tla 2 |23 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/the-nash-equilibrium[catachresis-colloquium/the-nash-equilibrium] |3 |0 |idris2 3 |59 |3 |0 |0 |0 |`docs/proof-debt.adoc`
+
+|https://github.com/hyperpolymath/BowtieRisk.jl[hyperpolymath/BowtieRisk.jl] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/Cliodynamics.jl[hyperpolymath/Cliodynamics.jl] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/Cliometrics.jl[hyperpolymath/Cliometrics.jl] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/SMTLib.jl[hyperpolymath/SMTLib.jl] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/affinescript-vite[hyperpolymath/affinescript-vite] |3 |0 |idris2 3 |32 |0 |0 |0 |0 |`.machine_readable/compliance/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/checky-monkey[hyperpolymath/checky-monkey] |3 |0 |idris2 3 |33 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/cicd-squabbler[hyperpolymath/cicd-squabbler] |3 |0 |spark 2, other 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/cloudguard-cli[hyperpolymath/cloudguard-cli] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/cloudguard-server[hyperpolymath/cloudguard-server] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/cookie-rebound[hyperpolymath/cookie-rebound] |3 |0 |idris2 3 |83 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/czech-file-knife[hyperpolymath/czech-file-knife] |3 |0 |spark 2, other 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/explicit-trust-plane[hyperpolymath/explicit-trust-plane] |3 |0 |idris2 3 |47 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/ffmpeg-ffi[hyperpolymath/ffmpeg-ffi] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/glyphbase[hyperpolymath/glyphbase] |3 |0 |idris2 3 |53 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/hpm-github-api-rsr[hyperpolymath/hpm-github-api-rsr] |3 |0 |idris2 3 |28 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/hpm-http-client-rsr[hyperpolymath/hpm-http-client-rsr] |3 |0 |idris2 3 |17 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/hpm-json-rsr[hyperpolymath/hpm-json-rsr] |3 |0 |idris2 3 |26 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/i-human[hyperpolymath/i-human] |3 |0 |idris2 3 |47 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/intsoc-transactor[hyperpolymath/intsoc-transactor] |3 |0 |idris2 3 |59 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/nesy-solver[hyperpolymath/nesy-solver] |3 |0 |idris2 3 |59 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/patch-bridge[hyperpolymath/patch-bridge] |3 |0 |idris2 3 |8 |1 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/pimcore-fortress[hyperpolymath/pimcore-fortress] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/unified-dataset-vocab[hyperpolymath/unified-dataset-vocab] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/universal-extension-format[hyperpolymath/universal-extension-format] |3 |0 |idris2 3 |60 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/universal-project-manager[hyperpolymath/universal-project-manager] |3 |0 |idris2 3 |47 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/volumod[hyperpolymath/volumod] |3 |0 |idris2 3 |58 |3 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/voyage-enterprise-decision-system[hyperpolymath/voyage-enterprise-decision-system] |3 |0 |idris2 3 |33 |0 |0 |0 |0 |—
+
+|https://github.com/metadatastician/authority-watch[metadatastician/authority-watch] |3 |0 |idris2 3 |13 |0 |0 |0 |0 |—
+
+|https://github.com/catachresis-colloquium/pong-ping[catachresis-colloquium/pong-ping] |2 |0 |idris2 2 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/sr71-blackglider[catachresis-colloquium/sr71-blackglider] |2 |0 |idris2 2 |21 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/feedback-o-tron[hyperpolymath/feedback-o-tron] |2 |0 |idris2 2 |38 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/git-reticulator[hyperpolymath/git-reticulator] |2 |0 |idris2 2 |10 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/launch-scaffolder[hyperpolymath/launch-scaffolder] |2 |2 |idris2 2 |1 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/nextgen-language-evangeliser[hyperpolymath/nextgen-language-evangeliser] |2 |0 |idris2 2 |15 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/phantom-metal-taste[hyperpolymath/phantom-metal-taste] |2 |0 |tla 2 |9 |0 |0 |0 |0 |—
+
+|https://github.com/metadatastician/selur[metadatastician/selur] |2 |0 |idris2 2 |23 |4 |0 |0 |0 |—
+
+|https://github.com/catachresis-colloquium/enterglide-ncc-137-k[catachresis-colloquium/enterglide-ncc-137-k] |1 |0 |idris2 1 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/planer-1[catachresis-colloquium/planer-1] |1 |0 |idris2 1 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/project-ovine[catachresis-colloquium/project-ovine] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/stealth-glider-ecosystem[catachresis-colloquium/stealth-glider-ecosystem] |1 |0 |idris2 1 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/tardis-rule-disruption[catachresis-colloquium/tardis-rule-disruption] |1 |0 |idris2 1 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/catachresis-colloquium/x15-rocket-glider[catachresis-colloquium/x15-rocket-glider] |1 |0 |idris2 1 |13 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/candy-crash[hyperpolymath/candy-crash] |1 |0 |idris2 1 |5 |0 |0 |0 |0 |—
+
+|https://github.com/hyperpolymath/dictask[hyperpolymath/dictask] |1 |0 |idris2 1 |17 |2 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/haec[hyperpolymath/haec] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/hermeneia[hyperpolymath/hermeneia] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/laminar[hyperpolymath/laminar] |1 |0 |idris2 1 |6 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/panoply[hyperpolymath/panoply] |1 |0 |idris2 1 |5 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/hyperpolymath/polyglot-formalisms-elixir[hyperpolymath/polyglot-formalisms-elixir] |1 |1 |idris2 1 |5 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/bowtie-workbench[metadatastician/bowtie-workbench] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/cadastra[metadatastician/cadastra] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/common-signal[metadatastician/common-signal] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/first-post[metadatastician/first-post] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/marid[metadatastician/marid] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/proglanging-languages[metadatastician/proglanging-languages] |1 |1 |idris2 1 |1 |0 |0 |0 |0 |—
+
+|https://github.com/metadatastician/sim-public-relations[metadatastician/sim-public-relations] |1 |0 |idris2 1 |0 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`
+
+|https://github.com/metadatastician/standards[metadatastician/standards] |1 |0 |idris2 1 |22 |0 |0 |0 |0 |`3-practice/PROOF-NEEDS.adoc`
+|===
+
+== Not reached
+
+These repositories could not be cloned (private, no credentials in the census
+session):
+
+* catachresis-colloquium/reflexive-ai-studio
+* hyperpolymath/007-lang
+* hyperpolymath/HOL
+* hyperpolymath/achievements-lab
+* hyperpolymath/ai-cli-lab
+* hyperpolymath/axel-protocol
+* hyperpolymath/blog-drafts
+* hyperpolymath/claude-config-vault
+* hyperpolymath/claude-memory
+* hyperpolymath/contractiles-a2-lab
+* hyperpolymath/cut-calculus
+* hyperpolymath/dev-notes-vault
+* hyperpolymath/dev-notes
+* hyperpolymath/dotfiles
+* hyperpolymath/echobox
+* hyperpolymath/email-octad-experiment
+* hyperpolymath/estate-scripts
+* hyperpolymath/frayed-knot-toolkit
+* hyperpolymath/fumble
+* hyperpolymath/git-seo
+* hyperpolymath/hottchpotch
+* hyperpolymath/hyperpolymath-sovereign-registry
+* hyperpolymath/info
+* hyperpolymath/jewell.nexus
+* hyperpolymath/jonathanjewell.dev
+* hyperpolymath/lcb-website
+* hyperpolymath/lfs-shared
+* hyperpolymath/linguist
+* hyperpolymath/memory-vault
+* hyperpolymath/poly-observability-mcp
+* hyperpolymath/polystack
+* hyperpolymath/rescript
+* hyperpolymath/squisher-corpus
+* hyperpolymath/this-ssg
+* hyperpolymath/tools
+* hyperpolymath/typefix-zero
+* hyperpolymath/vex-tools
diff --git a/docs/catalogue/census/catalogue-rows.jsonl b/docs/catalogue/census/catalogue-rows.jsonl
new file mode 100644
index 00000000..6bc76e5e
--- /dev/null
+++ b/docs/catalogue/census/catalogue-rows.jsonl
@@ -0,0 +1,239 @@
+{"axioms":0,"class":"engineering","declarations":120,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"catachresis-colloquium/IDApTIK","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":36,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"catachresis-colloquium/befunge93-vault-cracker","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":95,"fixture_files":3,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"catachresis-colloquium/enaction-engine","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/enterglide-ncc-137-k","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":124,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"catachresis-colloquium/evil-weevil","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":212,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"catachresis-colloquium/game-server-admin","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":25,"fixture_files":0,"holes":0,"own_files":3,"policy":3,"provers":"lean 3","repo":"catachresis-colloquium/megadog","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/planer-1","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"catachresis-colloquium/pong-ping","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":14,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"catachresis-colloquium/pow-the-game","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/project-ovine","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":46,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"catachresis-colloquium/proof-of-work","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":21,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"catachresis-colloquium/sr71-blackglider","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/stealth-glider-ecosystem","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/tardis-rule-disruption","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":59,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"catachresis-colloquium/the-nash-equilibrium","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"catachresis-colloquium/thejeffparadox","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":254,"fixture_files":0,"holes":0,"own_files":29,"policy":0,"provers":"idris2 25, spark 3, other 1","repo":"catachresis-colloquium/universal-modding-studio","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"catachresis-colloquium/x15-rocket-glider","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":23,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"idris2 2, spark 5, other 1","repo":"hyperpolymath/0patch-lsa-sentinel","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":131,"fixture_files":0,"holes":3,"own_files":11,"policy":0,"provers":"idris2 11","repo":"hyperpolymath/Axiom.jl","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/BowtieRisk.jl","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/Cliodynamics.jl","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/Cliometrics.jl","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":184,"fixture_files":0,"holes":0,"own_files":10,"policy":0,"provers":"agda 10","repo":"hyperpolymath/CompositionalCounts.jl","status_doc":"","unsafe":0}
+{"axioms":1,"class":"theory","declarations":51,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"agda 11","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":1,"class":"theory","declarations":236,"fixture_files":0,"holes":0,"own_files":15,"policy":6,"provers":"agda 15","repo":"hyperpolymath/ExactCounts.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":1,"class":"theory","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":1,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0}
+{"axioms":1,"class":"theory","declarations":83,"fixture_files":12,"holes":1,"own_files":17,"policy":1,"provers":"agda 17","repo":"hyperpolymath/JuliaPackageSpitter.jl","status_doc":"PROOF-NEEDS.adoc","unsafe":1}
+{"axioms":0,"class":"theory","declarations":1,"fixture_files":1,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/ResidualEvidenceTypes.jl","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/SMTLib.jl","status_doc":"","unsafe":0}
+{"axioms":89,"class":"theory","declarations":950,"fixture_files":0,"holes":7,"own_files":40,"policy":4,"provers":"agda 5, lean 11, rocq 16, isabelle 2, idris2 5, smt-atp 1","repo":"hyperpolymath/absolute-zero","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":128,"fixture_files":2,"holes":1,"own_files":8,"policy":0,"provers":"idris2 8","repo":"hyperpolymath/aerie","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":1,"class":"theory","declarations":568,"fixture_files":0,"holes":9,"own_files":54,"policy":0,"provers":"agda 23, lean 1, rocq 21, idris2 9","repo":"hyperpolymath/affinescript","status_doc":"docs/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":32,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/affinescript-vite","status_doc":".machine_readable/compliance/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/affinescriptiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":139,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/alloyiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":777,"fixture_files":1,"holes":39,"own_files":102,"policy":0,"provers":"idris2 39, spark 58, other 5","repo":"hyperpolymath/ambientops","status_doc":"PROOF-NEEDS.adoc","unsafe":8}
+{"axioms":0,"class":"engineering","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/anvomidaviser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":80,"fixture_files":1,"holes":0,"own_files":14,"policy":0,"provers":"idris2 14","repo":"hyperpolymath/anytype","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":15,"fixture_files":32,"holes":0,"own_files":32,"policy":0,"provers":"agda 13, lean 2, rocq 4, isabelle 4, idris2 7, smt-atp 2","repo":"hyperpolymath/arghda-core","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":11340,"fixture_files":0,"holes":567,"own_files":567,"policy":0,"provers":"idris2 567","repo":"hyperpolymath/asdf-tool-plugins","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":127,"fixture_files":0,"holes":0,"own_files":21,"policy":4,"provers":"agda 4, idris2 3, smt-atp 14","repo":"hyperpolymath/atoma","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/atsiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":7,"fixture_files":1,"holes":0,"own_files":4,"policy":0,"provers":"agda 4","repo":"hyperpolymath/autoformal-fidelity","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":29,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/bebop-ffi","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":95,"fixture_files":9,"holes":0,"own_files":14,"policy":0,"provers":"lean 3, idris2 11","repo":"hyperpolymath/betlang","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":173,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/betlangiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":39,"policy":0,"provers":"spark 37, other 2","repo":"hyperpolymath/bitfuckit","status_doc":"","unsafe":2}
+{"axioms":0,"class":"engineering","declarations":166,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/bofig","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":46,"fixture_files":0,"holes":1,"own_files":8,"policy":0,"provers":"lean 8","repo":"hyperpolymath/boinc-boinc","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":421,"fixture_files":0,"holes":4,"own_files":26,"policy":0,"provers":"idris2 19, tla 6, alloy 1","repo":"hyperpolymath/boj-server","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":1500,"fixture_files":0,"holes":0,"own_files":184,"policy":0,"provers":"idris2 184","repo":"hyperpolymath/boj-server-cartridges","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":132,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/bqniser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":5,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/candy-crash","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/chapeliser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":33,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/checky-monkey","status_doc":"","unsafe":0}
+{"axioms":1,"class":"theory","declarations":178,"fixture_files":6,"holes":0,"own_files":25,"policy":1,"provers":"agda 25","repo":"hyperpolymath/choreographic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"spark 2, other 1","repo":"hyperpolymath/cicd-squabbler","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":46,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"idris2 4, spark 8, other 1","repo":"hyperpolymath/civic-connect","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":2,"holes":0,"own_files":4,"policy":0,"provers":"spark 3, other 1","repo":"hyperpolymath/cloud-sync-tuner","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/cloudguard-cli","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/cloudguard-server","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":23,"fixture_files":0,"holes":3,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/conative-gating","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":8,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"tla 6","repo":"hyperpolymath/conflow","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":15,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/continuation-mesh","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":36,"policy":0,"provers":"spark 34, other 2","repo":"hyperpolymath/contractiles","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":83,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/cookie-rebound","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"spark 2, other 1","repo":"hyperpolymath/czech-file-knife","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":146,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/dafniser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":118,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/ddraig-ssg","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":161,"fixture_files":0,"holes":0,"own_files":18,"policy":0,"provers":"idris2 15, spark 3","repo":"hyperpolymath/deed-core","status_doc":"","unsafe":10}
+{"axioms":0,"class":"engineering","declarations":99,"fixture_files":3,"holes":0,"own_files":8,"policy":0,"provers":"idris2 8","repo":"hyperpolymath/deed-ecosystem","status_doc":"deno/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":4024,"fixture_files":41,"holes":91,"own_files":722,"policy":2,"provers":"agda 2, lean 3, rocq 274, idris2 347, spark 91, tla 2, other 3","repo":"hyperpolymath/developer-ecosystem","status_doc":"PROOF-NEEDS.adoc","unsafe":61}
+{"axioms":0,"class":"engineering","declarations":17,"fixture_files":0,"holes":2,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/dictask","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"spark 10, other 1","repo":"hyperpolymath/docmatrix","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":223,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"idris2 7, spark 5, other 1","repo":"hyperpolymath/docudactyl","status_doc":"","unsafe":0}
+{"axioms":1,"class":"engineering","declarations":1885,"fixture_files":21,"holes":4,"own_files":167,"policy":23,"provers":"agda 24, lean 17, rocq 9, isabelle 6, idris2 49, spark 18, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4","repo":"hyperpolymath/echidna","status_doc":"docs/PROOF-NEEDS.adoc","unsafe":4}
+{"axioms":0,"class":"theory","declarations":63,"fixture_files":0,"holes":6,"own_files":7,"policy":0,"provers":"lean 2, rocq 2, idris2 3","repo":"hyperpolymath/echidnabot","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":1,"class":"theory","declarations":1467,"fixture_files":0,"holes":0,"own_files":148,"policy":1,"provers":"agda 148","repo":"hyperpolymath/echo-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":5,"class":"theory","declarations":218,"fixture_files":0,"holes":0,"own_files":11,"policy":1,"provers":"agda 1, rocq 6, idris2 4","repo":"hyperpolymath/eclexia","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":121,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/eclexiaiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":635,"fixture_files":0,"holes":15,"own_files":43,"policy":0,"provers":"rocq 19, idris2 24","repo":"hyperpolymath/ephapax","status_doc":"PROOF-NEEDS.adoc","unsafe":1}
+{"axioms":0,"class":"engineering","declarations":133,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ephapaxiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":320,"fixture_files":14,"holes":0,"own_files":37,"policy":0,"provers":"agda 37","repo":"hyperpolymath/epistemic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":57,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/error-lang","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/explicit-trust-plane","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":38,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/feedback-o-tron","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/ffmpeg-ffi","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":156,"fixture_files":0,"holes":0,"own_files":10,"policy":0,"provers":"idris2 10","repo":"hyperpolymath/fireflag","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":1,"class":"theory","declarations":409,"fixture_files":0,"holes":0,"own_files":38,"policy":0,"provers":"agda 19, lean 19","repo":"hyperpolymath/firmboot","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":47,"fixture_files":0,"holes":3,"own_files":14,"policy":0,"provers":"idris2 3, spark 9, other 2","repo":"hyperpolymath/flatracoon","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"spark 10, other 1","repo":"hyperpolymath/formatrix-docs","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/futharkiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":10,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/git-reticulator","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":63,"fixture_files":0,"holes":6,"own_files":7,"policy":0,"provers":"lean 2, rocq 2, idris2 3","repo":"hyperpolymath/gitbot-fleet","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/glyphbase","status_doc":"","unsafe":0}
+{"axioms":7,"class":"theory","declarations":737,"fixture_files":8,"holes":5,"own_files":53,"policy":0,"provers":"lean 49, idris2 4","repo":"hyperpolymath/gnpl","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/haec","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":161,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/halideiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/hermeneia","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":24,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/hpm-crypto-rsr","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":28,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/hpm-github-api-rsr","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":17,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/hpm-http-client-rsr","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":26,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/hpm-json-rsr","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":59,"fixture_files":0,"holes":1,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/http-capability-gateway","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":66,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/hybrid-automation-router","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":1,"class":"engineering","declarations":448,"fixture_files":11,"holes":3,"own_files":42,"policy":1,"provers":"agda 1, lean 7, rocq 1, idris2 29, spark 1, tla 2, other 1","repo":"hyperpolymath/hypatia","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/i-human","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":77,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/ideas-to-alphas","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":122,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/idrisiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":59,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/intsoc-transactor","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":8,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/invariant-path","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":17,"fixture_files":4,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/ipfs-overlay","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":254,"fixture_files":0,"holes":0,"own_files":18,"policy":0,"provers":"idris2 18","repo":"hyperpolymath/iseriser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":142,"fixture_files":5,"holes":0,"own_files":11,"policy":0,"provers":"agda 3, idris2 8","repo":"hyperpolymath/januskey","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":225,"fixture_files":0,"holes":0,"own_files":10,"policy":0,"provers":"lean 9, idris2 1","repo":"hyperpolymath/jtv-lang","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":399,"fixture_files":0,"holes":15,"own_files":25,"policy":0,"provers":"idris2 25","repo":"hyperpolymath/julia-ecosystem","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":18,"fixture_files":3,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/julia-professional-registry","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/julianiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":76,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/k9-ecosystem","status_doc":"deno/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":27,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 5","repo":"hyperpolymath/kaldor-iiot","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":105,"fixture_files":0,"holes":1,"own_files":13,"policy":0,"provers":"idris2 13","repo":"hyperpolymath/kategoria","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":4,"class":"theory","declarations":82,"fixture_files":0,"holes":0,"own_files":6,"policy":1,"provers":"agda 5, idris2 1","repo":"hyperpolymath/kitchenspeak","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":61,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"agda 2, idris2 3","repo":"hyperpolymath/krl","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":6,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/laminar","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":32,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"idris2 7, alloy 1","repo":"hyperpolymath/laniakea","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":1,"fixture_files":2,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/launch-scaffolder","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":264,"fixture_files":0,"holes":1,"own_files":13,"policy":0,"provers":"lean 8, idris2 5","repo":"hyperpolymath/lithoglyph","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":2,"class":"engineering","declarations":314,"fixture_files":0,"holes":0,"own_files":18,"policy":2,"provers":"agda 3, idris2 15","repo":"hyperpolymath/lol","status_doc":"docs/proof-debt.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":141,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/lustreiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":11,"fixture_files":2,"holes":0,"own_files":9,"policy":2,"provers":"agda 3, spark 4, other 2","repo":"hyperpolymath/maa-framework","status_doc":"PROOF-NEEDS.adoc","unsafe":1}
+{"axioms":0,"class":"theory","declarations":161,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"lean 15","repo":"hyperpolymath/marches","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":2,"holes":0,"own_files":12,"policy":0,"provers":"spark 9, other 3","repo":"hyperpolymath/modshells","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":26,"class":"theory","declarations":617,"fixture_files":0,"holes":0,"own_files":25,"policy":0,"provers":"rocq 16, idris2 9","repo":"hyperpolymath/my-lang","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":135,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/mylangiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":59,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/nesy-solver","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"hyperpolymath/network-ambulance","status_doc":"","unsafe":1}
+{"axioms":0,"class":"theory","declarations":19,"fixture_files":0,"holes":0,"own_files":6,"policy":6,"provers":"lean 3, tla 2, dafny 1","repo":"hyperpolymath/neurophone","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":279,"fixture_files":3,"holes":0,"own_files":24,"policy":0,"provers":"idris2 24","repo":"hyperpolymath/nextgen-databases","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":15,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/nextgen-language-evangeliser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":16,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"hyperpolymath/nextgen-typing","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/nimiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":156,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/oblibeniser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":99,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/oblibeny","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":76,"fixture_files":2,"holes":0,"own_files":19,"policy":0,"provers":"agda 8, lean 5, idris2 6","repo":"hyperpolymath/occupancy-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":404,"fixture_files":8,"holes":0,"own_files":48,"policy":0,"provers":"idris2 48","repo":"hyperpolymath/ochrance","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":123,"fixture_files":0,"holes":0,"own_files":14,"policy":0,"provers":"idris2 14","repo":"hyperpolymath/ochrance-framework","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":41,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/odds-and-sods-package-manager","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":157,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/otpiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":3,"fixture_files":4,"holes":0,"own_files":5,"policy":0,"provers":"agda 5","repo":"hyperpolymath/palimpsest-license","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":46,"fixture_files":1,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/panic-attack","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":125,"fixture_files":6,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/panll","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":5,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/panoply","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":113,"fixture_files":0,"holes":6,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/patallm-gallery","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":8,"fixture_files":0,"holes":1,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/patch-bridge","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":9,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"tla 2","repo":"hyperpolymath/phantom-metal-taste","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":140,"fixture_files":0,"holes":3,"own_files":12,"policy":2,"provers":"agda 3, lean 3, rocq 1, idris2 2, tla 3","repo":"hyperpolymath/phronesis","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":155,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/phronesiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/pimcore-fortress","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":5,"fixture_files":1,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"hyperpolymath/polyglot-formalisms-elixir","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"spark 10, other 1","repo":"hyperpolymath/polyglot-i18n","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ponyiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":76,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/presswerk","status_doc":"","unsafe":0}
+{"axioms":2,"class":"theory","declarations":365,"fixture_files":0,"holes":2,"own_files":42,"policy":0,"provers":"agda 10, lean 4, rocq 4, isabelle 2, idris2 12, tla 6, smt-atp 4","repo":"hyperpolymath/protocol-squisher","status_doc":"provenance/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":11166,"fixture_files":61,"holes":22,"own_files":967,"policy":0,"provers":"lean 14, idris2 906, spark 42, tla 1, other 4","repo":"hyperpolymath/proven","status_doc":"PROOF-NEEDS.adoc","unsafe":10}
+{"axioms":0,"class":"engineering","declarations":6242,"fixture_files":0,"holes":3,"own_files":1097,"policy":0,"provers":"idris2 899, spark 197, other 1","repo":"hyperpolymath/proven-servers","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":857,"fixture_files":27,"holes":0,"own_files":72,"policy":0,"provers":"idris2 72","repo":"hyperpolymath/proven-tests-and-benches","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":36,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"agda 1, idris2 1, tla 3","repo":"hyperpolymath/quandledb","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":20,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 2, tla 2","repo":"hyperpolymath/quintessence","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":59,"fixture_files":0,"holes":0,"own_files":22,"policy":0,"provers":"idris2 3, spark 18, other 1","repo":"hyperpolymath/raze-tui","status_doc":"","unsafe":2}
+{"axioms":0,"class":"engineering","declarations":7,"fixture_files":1,"holes":0,"own_files":16,"policy":0,"provers":"idris2 1, spark 13, other 2","repo":"hyperpolymath/reposystem","status_doc":"PROOF-NEEDS.adoc","unsafe":2}
+{"axioms":0,"class":"theory","declarations":328,"fixture_files":13,"holes":0,"own_files":27,"policy":0,"provers":"agda 27","repo":"hyperpolymath/residual-evidence-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":271,"fixture_files":12,"holes":0,"own_files":22,"policy":0,"provers":"agda 22","repo":"hyperpolymath/resource-algebra","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":32,"policy":0,"provers":"spark 31, other 1","repo":"hyperpolymath/resource-record-fluctuator","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":64,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"idris2 6, spark 6, other 1","repo":"hyperpolymath/robodog-defensive-systems-lab","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":74,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/rpa-elysium","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":67,"fixture_files":3,"holes":0,"own_files":16,"policy":0,"provers":"agda 16","repo":"hyperpolymath/secret-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":117,"fixture_files":0,"holes":3,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/session-sentinel","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":101,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/smtp-notify-action","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":43,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 2, idris2 1","repo":"hyperpolymath/snifs","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"spark 6, other 1","repo":"hyperpolymath/somethings-fishy","status_doc":"PROOF-NEEDS.adoc","unsafe":2}
+{"axioms":0,"class":"engineering","declarations":108,"fixture_files":0,"holes":3,"own_files":23,"policy":0,"provers":"lean 1, idris2 6, spark 13, other 3","repo":"hyperpolymath/ssg-collection","status_doc":"PROOF-NEEDS.adoc","unsafe":4}
+{"axioms":0,"class":"engineering","declarations":23,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 2, tla 2","repo":"hyperpolymath/stateful-artefacts","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":22,"fixture_files":0,"holes":0,"own_files":4,"policy":3,"provers":"agda 4","repo":"hyperpolymath/statistikles","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":164,"fixture_files":0,"holes":0,"own_files":21,"policy":0,"provers":"lean 21","repo":"hyperpolymath/system-et","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":61,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"lean 3","repo":"hyperpolymath/tangle","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":74,"fixture_files":9,"holes":0,"own_files":10,"policy":0,"provers":"idris2 10","repo":"hyperpolymath/thunderbird-template-reloaded","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":181,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/tlaiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":16,"policy":0,"provers":"spark 15, other 1","repo":"hyperpolymath/tree-navigator","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":13,"class":"engineering","declarations":165,"fixture_files":20,"holes":0,"own_files":64,"policy":0,"provers":"agda 2, idris2 5, spark 56, other 1","repo":"hyperpolymath/trigger","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":492,"fixture_files":0,"holes":10,"own_files":37,"policy":1,"provers":"agda 10, lean 11, idris2 16","repo":"hyperpolymath/trope-checker","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":540,"fixture_files":0,"holes":5,"own_files":28,"policy":0,"provers":"lean 19, isabelle 9","repo":"hyperpolymath/tropical-types","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":850,"fixture_files":12,"holes":0,"own_files":46,"policy":0,"provers":"idris2 46","repo":"hyperpolymath/typed-wasm","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":155,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"idris2 11","repo":"hyperpolymath/typedqliser","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":159,"fixture_files":0,"holes":3,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/typell","status_doc":"PROOF-STATUS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":76,"fixture_files":6,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/ubicity","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/unified-dataset-vocab","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":110,"fixture_files":9,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/universal-chat-extractor","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/universal-extension-format","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/universal-project-manager","status_doc":"","unsafe":0}
+{"axioms":1,"class":"theory","declarations":960,"fixture_files":0,"holes":5,"own_files":64,"policy":9,"provers":"agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5","repo":"hyperpolymath/valence-shell","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":953,"fixture_files":15,"holes":0,"own_files":36,"policy":0,"provers":"idris2 36","repo":"hyperpolymath/vcl-ut","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":51,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/veridical-simulation-core","status_doc":"","unsafe":0}
+{"axioms":43,"class":"engineering","declarations":365,"fixture_files":0,"holes":3,"own_files":20,"policy":0,"provers":"rocq 9, idris2 11","repo":"hyperpolymath/verisimdb","status_doc":"docs/proof-debt.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":208,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/verisimiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":104,"fixture_files":6,"holes":3,"own_files":42,"policy":0,"provers":"idris2 10, spark 29, other 3","repo":"hyperpolymath/vexometer","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":58,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/volumod","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":33,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/voyage-enterprise-decision-system","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":418,"fixture_files":0,"holes":0,"own_files":18,"policy":0,"provers":"lean 7, rocq 3, idris2 8","repo":"hyperpolymath/wokelang","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":143,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/wokelangiser","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":16,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"isabelle 1","repo":"hyperpolymath/zerostep","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":110,"fixture_files":8,"holes":3,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/zerotier-k8s-link","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":94,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"lean 9, idris2 3, tla 3","repo":"hyperpolymath/zotero-tools","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"theory","declarations":70,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"agda 13","repo":"metadatastician/MetaManifold-Evidence","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"metadatastician/ZenodoDeposits.jl","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":70,"fixture_files":0,"holes":3,"own_files":34,"policy":0,"provers":"idris2 5, spark 25, other 4","repo":"metadatastician/_pathroot","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":13,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"metadatastician/authority-watch","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/bowtie-workbench","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":127,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"metadatastician/burble","status_doc":"PROOF-NEEDS.md","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/cadastra","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":91,"fixture_files":1,"holes":18,"own_files":85,"policy":0,"provers":"idris2 8, spark 75, other 2","repo":"metadatastician/cerro-torre","status_doc":"","unsafe":69}
+{"axioms":0,"class":"engineering","declarations":38,"fixture_files":3,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"metadatastician/cleave","status_doc":"docs/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/common-signal","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/first-post","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":1868,"fixture_files":10,"holes":0,"own_files":62,"policy":0,"provers":"idris2 53, tla 9","repo":"metadatastician/gossamer","status_doc":"PROOF-NEEDS.md","unsafe":8}
+{"axioms":0,"class":"engineering","declarations":185,"fixture_files":3,"holes":0,"own_files":19,"policy":0,"provers":"idris2 19","repo":"metadatastician/groove","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":108,"fixture_files":3,"holes":0,"own_files":9,"policy":0,"provers":"agda 5, idris2 1, tla 3","repo":"metadatastician/hvn-dehallucinator","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":25,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"metadatastician/insolvency-tycoon","status_doc":"","unsafe":0}
+{"axioms":0,"class":"theory","declarations":58,"fixture_files":4,"holes":0,"own_files":6,"policy":0,"provers":"agda 6","repo":"metadatastician/lintel","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/marid","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":991,"fixture_files":8,"holes":4,"own_files":51,"policy":2,"provers":"agda 2, lean 1, idris2 42, tla 6","repo":"metadatastician/paint-type","status_doc":"PROOF-NEEDS.adoc","unsafe":8}
+{"axioms":4,"class":"engineering","declarations":199,"fixture_files":0,"holes":0,"own_files":11,"policy":0,"provers":"lean 5, idris2 6","repo":"metadatastician/phi-LAM","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":1,"fixture_files":1,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/proglanging-languages","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":23,"fixture_files":0,"holes":4,"own_files":2,"policy":0,"provers":"idris2 2","repo":"metadatastician/selur","status_doc":"","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/sim-public-relations","status_doc":"docs/status/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":22,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/standards","status_doc":"3-practice/PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":294,"fixture_files":8,"holes":0,"own_files":19,"policy":0,"provers":"idris2 18, alloy 1","repo":"metadatastician/stapeln","status_doc":"PROOF-NEEDS.adoc","unsafe":0}
+{"axioms":0,"class":"engineering","declarations":122,"fixture_files":2,"holes":0,"own_files":23,"policy":0,"provers":"idris2 10, spark 12, other 1","repo":"metadatastician/vordr","status_doc":"","unsafe":4}
diff --git a/docs/catalogue/census/repos.jsonl b/docs/catalogue/census/repos.jsonl
new file mode 100644
index 00000000..6c430d6d
--- /dev/null
+++ b/docs/catalogue/census/repos.jsonl
@@ -0,0 +1,476 @@
+{"fork":false,"full_name":"catachresis-colloquium/688-attack-hub","pushed_at":"2026-10-12T23:21:22Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/IDApTIK","pushed_at":"2026-10-26T07:38:43Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/airborne-submarine-squadron","pushed_at":"2026-10-20T16:34:28Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/befunge93-vault-cracker","pushed_at":"2026-10-25T22:29:04Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/blue-screen-of-app","pushed_at":"2026-10-10T15:55:03Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/chronicles-of-slavia","pushed_at":"2026-10-01T13:47:25Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/dosovoi","pushed_at":"2026-10-01T14:14:49Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/enaction-engine","pushed_at":"2026-10-25T22:43:40Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/enterglide-ncc-137-k","pushed_at":"2026-10-02T15:00:59Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/evil-weevil","pushed_at":"2026-10-18T08:57:54Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/f117a-stealth-glider","pushed_at":"2026-10-12T23:21:07Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/f19-stealth-glider","pushed_at":"2026-10-12T23:23:48Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/first-post","pushed_at":"2026-10-12T23:07:04Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/game-server-admin","pushed_at":"2026-10-26T03:52:40Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/hotchocolabot","pushed_at":"2026-10-01T11:05:55Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/knot-rider","pushed_at":"2026-10-22T10:52:18Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/megadog","pushed_at":"2026-10-12T23:04:27Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/not-so-serious-software","pushed_at":"2026-10-01T21:41:47Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/planer-1","pushed_at":"2026-10-02T18:52:02Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/pong-ping","pushed_at":"2026-10-12T23:19:34Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/pow-the-game","pushed_at":"2026-10-12T23:03:55Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/project-ovine","pushed_at":"2026-10-18T02:15:04Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/proof-of-work","pushed_at":"2026-10-22T13:24:00Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/reflexive-ai-studio","pushed_at":"2026-09-15T19:36:33Z","visibility":"private"}
+{"fork":false,"full_name":"catachresis-colloquium/sr71-blackglider","pushed_at":"2026-10-12T23:24:28Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/stealth-glider-ecosystem","pushed_at":"2026-10-02T14:33:40Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/tardis-rule-disruption","pushed_at":"2026-10-02T14:35:24Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/the-nash-equilibrium","pushed_at":"2026-10-26T00:46:49Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/thejeffparadox","pushed_at":"2026-10-22T14:11:05Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/universal-modding-studio","pushed_at":"2026-10-25T14:02:08Z","visibility":"public"}
+{"fork":false,"full_name":"catachresis-colloquium/x15-rocket-glider","pushed_at":"2026-10-01T23:11:29Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/007-lang","pushed_at":"2026-10-26T07:40:03Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/0patch-lsa-sentinel","pushed_at":"2026-10-01T19:53:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/AcceleratorGate.jl","pushed_at":"2026-10-20T22:41:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Apodeixis.jl","pushed_at":"2026-10-22T17:35:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Axiology.jl","pushed_at":"2026-10-22T00:45:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Axiom.jl","pushed_at":"2026-10-22T19:50:29Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/BowtieRisk.jl","pushed_at":"2026-10-20T22:20:39Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Causals.jl","pushed_at":"2026-10-20T00:38:27Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Cladistics.jl","pushed_at":"2026-10-24T11:19:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Cliodynamics.jl","pushed_at":"2026-10-24T11:17:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Cliometrics.jl","pushed_at":"2026-10-22T00:43:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/CompositionalCounts.jl","pushed_at":"2026-10-15T15:43:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/CompositionalDA.jl","pushed_at":"2026-10-15T19:51:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ContrastFamilies.jl","pushed_at":"2026-10-02T08:32:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/CoprocessorRuntime.jl","pushed_at":"2026-10-24T09:04:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/EchoTypes.jl","pushed_at":"2026-10-20T22:27:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/EpistemicTypes.jl","pushed_at":"2026-10-24T11:18:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ExactCounts.jl","pushed_at":"2026-10-06T17:30:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ExactTests.jl","pushed_at":"2026-10-06T10:13:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Exnovation.jl","pushed_at":"2026-10-24T11:18:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/FirmwareAudit.jl","pushed_at":"2026-10-20T09:13:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/HOL","pushed_at":"2026-10-01T14:53:07Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/HackenbushGames.jl","pushed_at":"2026-10-25T08:10:24Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/HardwareResilience.jl","pushed_at":"2026-10-20T13:20:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Hyperpolymath.jl","pushed_at":"2026-10-24T11:19:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/InvestigativeJournalism.jl","pushed_at":"2026-10-09T11:08:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/JuliaKids.jl","pushed_at":"2026-10-24T11:18:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/JuliaPackageSpitter.jl","pushed_at":"2026-10-22T00:46:44Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/KnotTheory.jl","pushed_at":"2026-10-20T10:07:58Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/LowLevel.jl","pushed_at":"2026-10-20T06:24:00Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/MacroPower.jl","pushed_at":"2026-10-20T01:25:08Z","visibility":"public"}
+{"fork":true,"full_name":"hyperpolymath/MetaManifold-WebUI","pushed_at":"2026-10-26T07:46:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/PRComms.jl","pushed_at":"2026-10-01T23:06:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/PolyglotFormalisms.jl","pushed_at":"2026-10-26T10:11:25Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/PostDisciplinary.jl","pushed_at":"2026-10-24T11:18:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Protoctist.jl","pushed_at":"2026-10-21T14:57:24Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/QuantumCircuit.jl","pushed_at":"2026-10-24T11:18:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ResidualEvidenceTypes.jl","pushed_at":"2026-10-24T11:19:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/SMTLib.jl","pushed_at":"2026-10-26T11:48:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ShellIntegration.jl","pushed_at":"2026-10-20T22:38:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/SiliconCore.jl","pushed_at":"2026-10-20T08:43:56Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/Skein.jl","pushed_at":"2026-10-25T08:09:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/SoftwareSovereign.jl","pushed_at":"2026-10-20T04:43:58Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/TradeUnionism.jl","pushed_at":"2026-10-01T19:41:58Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ViableSystems.jl","pushed_at":"2026-10-25T08:10:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ZeroProb.jl","pushed_at":"2026-10-21T17:36:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/absolute-zero","pushed_at":"2026-10-23T22:11:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/academic-workflow-suite","pushed_at":"2026-10-26T06:10:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/accessibility-everywhere","pushed_at":"2026-10-23T07:15:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/achievements-lab","pushed_at":"2026-10-01T19:53:52Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/action-trust-layers","pushed_at":"2026-10-11T05:04:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/aerie","pushed_at":"2026-10-01T17:35:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/affinescript","pushed_at":"2026-10-17T16:55:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/affinescript-vite","pushed_at":"2026-10-01T23:41:39Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/affinescriptiser","pushed_at":"2026-10-23T13:50:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/aggregate-library","pushed_at":"2026-10-14T07:18:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ai-cli-lab","pushed_at":"2026-10-03T15:06:34Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/alloyiser","pushed_at":"2026-10-23T07:16:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ambientops","pushed_at":"2026-10-22T20:28:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/anamnesis","pushed_at":"2026-10-16T16:15:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/anvomidav","pushed_at":"2026-10-20T22:18:16Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/anvomidaviser","pushed_at":"2026-10-16T20:55:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/anytype","pushed_at":"2026-10-23T07:09:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/arghda-core","pushed_at":"2026-10-01T20:53:20Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/asdf-tool-plugins","pushed_at":"2026-10-25T21:44:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/aspasia","pushed_at":"2026-10-01T23:42:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/atoma","pushed_at":"2026-10-22T17:07:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/atsiser","pushed_at":"2026-10-24T00:48:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/autoformal-fidelity","pushed_at":"2026-10-19T20:24:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/axel-protocol","pushed_at":"2026-10-01T19:39:22Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/bactrian","pushed_at":"2026-10-22T17:49:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bebop-ffi","pushed_at":"2026-10-23T10:44:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/betlang","pushed_at":"2026-10-26T00:51:26Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/betlangiser","pushed_at":"2026-10-23T17:52:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bgp-backbone-lab","pushed_at":"2026-10-13T21:41:16Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bitfuckit","pushed_at":"2026-10-26T06:57:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/blocky-writer","pushed_at":"2026-10-19T21:57:50Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/blog-drafts","pushed_at":"2026-10-01T20:10:31Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/bofig","pushed_at":"2026-10-23T06:18:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bofj-kitt","pushed_at":"2026-10-19T21:28:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/boinc-boinc","pushed_at":"2026-10-01T20:11:11Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/boj-server","pushed_at":"2026-10-23T02:28:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/boj-server-cartridges","pushed_at":"2026-10-26T07:37:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bqniser","pushed_at":"2026-10-23T07:15:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/branch-newspaper","pushed_at":"2026-10-01T23:47:14Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/bunsenite","pushed_at":"2026-10-23T17:53:54Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cafescripto","pushed_at":"2026-10-24T20:51:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/candy-crash","pushed_at":"2026-10-03T10:15:37Z","visibility":"public"}
+{"fork":true,"full_name":"hyperpolymath/cargo-zigbuild","pushed_at":"2026-10-02T18:19:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/casket-ssg","pushed_at":"2026-10-13T04:17:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cccp","pushed_at":"2026-10-23T15:28:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/chapeliser","pushed_at":"2026-10-23T23:21:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/checky-monkey","pushed_at":"2026-10-22T05:56:42Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/chimichanga","pushed_at":"2026-10-22T21:47:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/choreographic-types","pushed_at":"2026-10-19T22:14:38Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cicd-squabbler","pushed_at":"2026-10-26T07:33:13Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cicd-suite","pushed_at":"2026-10-19T20:23:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/civic-connect","pushed_at":"2026-10-02T01:05:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/claude-config-vault","pushed_at":"2026-10-09T13:39:04Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/claude-gecko-browser-extension","pushed_at":"2026-10-26T10:47:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/claude-integrations","pushed_at":"2026-10-10T10:19:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/claude-memory","pushed_at":"2026-10-01T19:39:00Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/cloud-sync-tuner","pushed_at":"2026-10-20T22:20:14Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cloudflare-dns-terraform","pushed_at":"2026-10-26T07:33:39Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cloudguard-cli","pushed_at":"2026-10-26T14:00:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cloudguard-server","pushed_at":"2026-10-01T20:20:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/conative-gating","pushed_at":"2026-10-03T10:26:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/conflow","pushed_at":"2026-10-26T07:34:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/continuation-mesh","pushed_at":"2026-10-25T10:26:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/contractiles","pushed_at":"2026-10-25T10:26:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/contractiles-a2-lab","pushed_at":"2026-10-01T20:26:27Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/cookie-rebound","pushed_at":"2026-10-26T02:47:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/coord-tui","pushed_at":"2026-10-24T22:42:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/coq-jr","pushed_at":"2026-10-17T21:13:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/cut-calculus","pushed_at":"2026-10-03T14:42:44Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/cyo","pushed_at":"2026-10-17T05:45:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/czech-file-knife","pushed_at":"2026-10-26T07:30:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/dafniser","pushed_at":"2026-10-23T07:06:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ddraig-ssg","pushed_at":"2026-10-13T23:57:39Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/deed-core","pushed_at":"2026-10-01T20:11:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/deed-ecosystem","pushed_at":"2026-10-25T10:26:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/deed-validate-action","pushed_at":"2026-10-15T08:22:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/defiant","pushed_at":"2026-10-01T23:46:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/dev-notes","pushed_at":"2026-10-01T20:22:10Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/dev-notes-vault","pushed_at":"2026-10-11T19:47:11Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/developer-ecosystem","pushed_at":"2026-10-22T00:34:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/dictask","pushed_at":"2026-10-24T10:06:38Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/dicti0nary-attack","pushed_at":"2026-10-24T20:51:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/docmatrix","pushed_at":"2026-10-14T03:55:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/docudactyl","pushed_at":"2026-10-23T00:56:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/dotfiles","pushed_at":"2026-10-01T20:14:07Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/dotmatrix-fileprinter","pushed_at":"2026-10-22T00:48:29Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/double-track-browser","pushed_at":"2026-10-20T22:41:38Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/echidna","pushed_at":"2026-10-23T08:09:26Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/echidnabot","pushed_at":"2026-10-23T13:50:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/echo-types","pushed_at":"2026-10-26T16:56:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/echobox","pushed_at":"2026-10-01T14:00:58Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/eclexia","pushed_at":"2026-10-24T14:16:04Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/eclexiaiser","pushed_at":"2026-10-23T19:00:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/email-octad-experiment","pushed_at":"2026-10-01T20:14:42Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/empty-linter","pushed_at":"2026-10-20T00:26:38Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ensaid-spec","pushed_at":"2026-10-13T04:33:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ephapax","pushed_at":"2026-10-26T07:33:58Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ephapaxiser","pushed_at":"2026-10-23T07:06:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/epistemic-types","pushed_at":"2026-10-25T22:16:24Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/error-lang","pushed_at":"2026-10-01T20:15:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/estate-scripts","pushed_at":"2026-10-09T00:34:55Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/excel-economic-numbers-tool","pushed_at":"2026-10-24T11:20:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/explicit-trust-plane","pushed_at":"2026-10-25T17:25:14Z","visibility":"public"}
+{"fork":true,"full_name":"hyperpolymath/explore","pushed_at":"2026-10-22T00:39:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/feedback-o-tron","pushed_at":"2026-10-20T14:29:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ffmpeg-ffi","pushed_at":"2026-10-26T07:33:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/filesoup","pushed_at":"2026-10-25T10:26:13Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/fireflag","pushed_at":"2026-10-21T23:19:13Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/firmboot","pushed_at":"2026-10-08T19:56:42Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/flat-mate","pushed_at":"2026-10-26T10:01:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/flatracoon","pushed_at":"2026-10-01T20:17:48Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/formatrix-docs","pushed_at":"2026-10-26T15:30:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/frayed-knot-toolkit","pushed_at":"2026-10-01T20:13:18Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/fraying-model-computational-testbed","pushed_at":"2026-10-22T05:55:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/fumble","pushed_at":"2026-10-14T06:11:54Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/futharkiser","pushed_at":"2026-10-23T07:05:51Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/git-reticulator","pushed_at":"2026-10-20T22:38:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/git-scripts","pushed_at":"2026-10-22T06:58:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/git-seo","pushed_at":"2026-10-01T20:13:43Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/gitbot-fleet","pushed_at":"2026-10-25T08:13:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/glyphbase","pushed_at":"2026-10-12T22:04:13Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/gnpl","pushed_at":"2026-10-12T22:07:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/grim-repo","pushed_at":"2026-10-17T03:04:27Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/gsbot","pushed_at":"2026-10-23T06:08:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/gv-clade-index","pushed_at":"2026-10-26T16:30:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/haec","pushed_at":"2026-10-21T15:06:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/halideiser","pushed_at":"2026-10-23T21:36:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hermeneia","pushed_at":"2026-10-23T13:47:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/heron-polyfeed-reader","pushed_at":"2026-10-20T08:10:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hesiod-dns-map","pushed_at":"2026-10-05T22:28:11Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/heterogenous-mobile-computing","pushed_at":"2026-10-17T14:04:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/homebrew-tap","pushed_at":"2026-10-23T07:06:20Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hottchpotch","pushed_at":"2026-10-18T02:14:51Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/hpm-crypto-rsr","pushed_at":"2026-10-01T21:22:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hpm-github-api-rsr","pushed_at":"2026-10-01T19:40:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hpm-http-client-rsr","pushed_at":"2026-10-01T14:02:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hpm-json-rsr","pushed_at":"2026-10-01T14:02:26Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/http-capability-gateway","pushed_at":"2026-10-20T22:13:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hybrid-automation-router","pushed_at":"2026-10-26T11:45:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hypatia","pushed_at":"2026-10-25T21:26:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hyperpolymath","pushed_at":"2026-10-12T22:09:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/hyperpolymath-sovereign-registry","pushed_at":"2026-10-01T20:17:42Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/hyperpolymath.github.io","pushed_at":"2026-10-13T06:43:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/i-human","pushed_at":"2026-10-01T21:19:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ideas-to-alphas","pushed_at":"2026-10-25T08:11:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/idrisiser","pushed_at":"2026-10-23T21:09:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ijson-jcs","pushed_at":"2026-10-25T20:40:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/im-docs","pushed_at":"2026-10-25T17:24:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/info","pushed_at":"2026-10-03T14:38:36Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/infrastructure-automation","pushed_at":"2026-10-14T01:57:48Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/intsoc-transactor","pushed_at":"2026-10-23T15:19:56Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/invariant-path","pushed_at":"2026-10-18T15:13:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ipfs-overlay","pushed_at":"2026-10-18T13:04:14Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ipv6-only","pushed_at":"2026-10-09T03:33:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ipv6-site-enforcer","pushed_at":"2026-10-12T23:50:50Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ipv6-tools","pushed_at":"2026-10-18T18:12:51Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/iseriser","pushed_at":"2026-10-23T07:19:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/jaffascript","pushed_at":"2026-10-24T08:16:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/januskey","pushed_at":"2026-10-22T05:55:05Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/jewell.nexus","pushed_at":"2026-10-01T19:39:16Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/jonathanjewell.dev","pushed_at":"2026-10-01T14:02:45Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/jtv-halting-islands-ct","pushed_at":"2026-10-12T18:43:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/jtv-lang","pushed_at":"2026-10-25T21:00:16Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/julia-ecosystem","pushed_at":"2026-10-01T21:44:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/julia-professional-registry","pushed_at":"2026-10-25T08:10:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/julianiser","pushed_at":"2026-10-23T21:12:16Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/k9-ecosystem","pushed_at":"2026-10-01T21:50:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/kaldor-iiot","pushed_at":"2026-10-23T17:52:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/kategoria","pushed_at":"2026-10-01T21:19:04Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/kea","pushed_at":"2026-10-26T07:35:14Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/kitchenspeak","pushed_at":"2026-10-20T13:20:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/krl","pushed_at":"2026-10-25T18:35:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/laminar","pushed_at":"2026-10-22T06:06:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/laniakea","pushed_at":"2026-10-20T13:21:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/launch-scaffolder","pushed_at":"2026-10-23T12:57:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/lcb-website","pushed_at":"2026-10-21T23:15:10Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/lfs-shared","pushed_at":"2026-10-01T21:20:44Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/linguist","pushed_at":"2026-10-01T21:20:36Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/lithoglyph","pushed_at":"2026-10-26T11:46:04Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/live-files","pushed_at":"2026-10-19T07:49:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/llm-grace","pushed_at":"2026-10-26T11:47:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/lol","pushed_at":"2026-10-15T22:39:15Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/lucidscript","pushed_at":"2026-10-24T20:52:26Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/lustreiser","pushed_at":"2026-10-23T16:47:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/maa-framework","pushed_at":"2026-10-22T13:40:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/manifesto","pushed_at":"2026-10-20T19:02:42Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/marches","pushed_at":"2026-10-26T07:47:15Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/me-dialect","pushed_at":"2026-10-01T21:36:32Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/memory-vault","pushed_at":"2026-10-09T14:30:05Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/metadata-grammar","pushed_at":"2026-10-17T03:44:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/methodologies","pushed_at":"2026-10-26T11:47:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/misinformation-defence-platform","pushed_at":"2026-10-02T00:56:31Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/modshells","pushed_at":"2026-10-26T07:31:04Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/my-lang","pushed_at":"2026-10-26T15:29:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/mylangiser","pushed_at":"2026-10-23T07:16:42Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nafa-app","pushed_at":"2026-10-23T16:47:44Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/natsci-studio","pushed_at":"2026-10-24T05:30:39Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nesy-solver","pushed_at":"2026-10-25T21:14:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/network-ambulance","pushed_at":"2026-10-23T22:45:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/network-dashboard","pushed_at":"2026-10-01T22:59:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/network-outpost","pushed_at":"2026-10-14T08:40:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/neural-foundations","pushed_at":"2026-10-01T21:38:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/neurophone","pushed_at":"2026-10-22T00:48:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nexia-list","pushed_at":"2026-10-22T03:08:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nextgen-databases","pushed_at":"2026-10-23T07:25:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nextgen-language-evangeliser","pushed_at":"2026-10-23T12:46:54Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nextgen-languages","pushed_at":"2026-10-25T08:11:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nextgen-typing","pushed_at":"2026-10-25T08:11:56Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nickel-augmentation","pushed_at":"2026-10-25T17:24:29Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/nimiser","pushed_at":"2026-10-23T13:46:11Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/no-nonsense-nntps","pushed_at":"2026-10-24T00:52:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/oblibeniser","pushed_at":"2026-10-23T19:22:20Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/oblibeny","pushed_at":"2026-10-12T22:06:27Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/occupancy-types","pushed_at":"2026-10-18T04:35:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ochrance","pushed_at":"2026-10-23T07:06:27Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ochrance-framework","pushed_at":"2026-10-20T13:18:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/odds-and-sods-package-manager","pushed_at":"2026-10-25T22:41:38Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/oikos-economics-accounting-dsl","pushed_at":"2026-10-24T05:31:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/oikosbot","pushed_at":"2026-10-23T17:44:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/oikosbot-estate","pushed_at":"2026-10-01T22:40:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ordinal-notation","pushed_at":"2026-10-26T16:52:30Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/otpiser","pushed_at":"2026-10-23T15:26:05Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/palimpsest-license","pushed_at":"2026-10-19T15:31:03Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/panic-attack","pushed_at":"2026-10-26T07:44:42Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/panll","pushed_at":"2026-10-26T12:46:44Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/panoply","pushed_at":"2026-10-25T07:53:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/patallm-gallery","pushed_at":"2026-10-24T15:46:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/patch-bridge","pushed_at":"2026-10-26T16:48:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/phantom-metal-taste","pushed_at":"2026-10-24T05:30:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/php-aegis","pushed_at":"2026-10-22T07:36:00Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/phronesis","pushed_at":"2026-10-25T17:38:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/phronesiser","pushed_at":"2026-10-23T13:46:49Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/pimcore-fortress","pushed_at":"2026-10-01T21:32:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/plasma-parser-writer","pushed_at":"2026-10-20T12:57:56Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/poly-k8s-mcp","pushed_at":"2026-10-23T14:54:59Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/poly-observability-mcp","pushed_at":"2026-10-01T15:30:39Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/polyglot-formalisms-elixir","pushed_at":"2026-10-26T07:34:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/polyglot-formalisms-gleam","pushed_at":"2026-10-14T04:47:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/polyglot-i18n","pushed_at":"2026-10-25T12:35:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/polysafe-gitfixer","pushed_at":"2026-10-24T05:31:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/polystack","pushed_at":"2026-10-01T21:31:31Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/pons-asinorum","pushed_at":"2026-10-25T22:36:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ponyiser","pushed_at":"2026-10-23T16:47:31Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/preference-injector","pushed_at":"2026-10-23T21:36:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/presswerk","pushed_at":"2026-10-23T21:07:32Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/project-wharf","pushed_at":"2026-10-22T00:37:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/proof-burrower","pushed_at":"2026-10-25T07:54:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/protocol-squisher","pushed_at":"2026-10-17T14:13:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/proven","pushed_at":"2026-10-07T11:15:27Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/proven-servers","pushed_at":"2026-10-25T21:16:23Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/proven-tests-and-benches","pushed_at":"2026-10-26T10:01:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/pseudoscript","pushed_at":"2026-10-17T07:56:00Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/quandledb","pushed_at":"2026-10-25T08:12:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/qubes-sdp","pushed_at":"2026-10-17T11:53:34Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/quintessence","pushed_at":"2026-10-22T17:28:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/rattlescript","pushed_at":"2026-10-24T02:10:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/raze-tui","pushed_at":"2026-10-13T06:23:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/reasonably-good-token-vault","pushed_at":"2026-10-26T13:55:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/recon-silly-ation","pushed_at":"2026-10-25T17:24:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/refugia","pushed_at":"2026-10-01T19:49:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/repo-guardian","pushed_at":"2026-10-01T14:07:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/reposystem","pushed_at":"2026-10-25T22:16:14Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/rescript","pushed_at":"2026-10-01T19:49:04Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/rescript-ecosystem","pushed_at":"2026-10-23T17:07:58Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/residual-evidence-types","pushed_at":"2026-10-12T20:20:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/resource-algebra","pushed_at":"2026-10-19T23:03:37Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/resource-record-fluctuator","pushed_at":"2026-10-23T07:35:48Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/robodog-defensive-systems-lab","pushed_at":"2026-10-23T07:55:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/robot-vacuum-cleaner","pushed_at":"2026-10-23T05:11:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/rpa-elysium","pushed_at":"2026-10-20T13:21:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/rrecord-verity","pushed_at":"2026-10-22T00:34:11Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/rsr-template-repo","pushed_at":"2026-10-25T22:09:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/safe-brute-force","pushed_at":"2026-10-24T22:18:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/sanctify-php","pushed_at":"2026-10-22T23:06:37Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/scaffoldia","pushed_at":"2026-10-25T21:15:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/scripts","pushed_at":"2026-10-26T11:46:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/sdp-hkdf-deployment","pushed_at":"2026-10-23T07:17:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/seamstress","pushed_at":"2026-10-26T07:33:32Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/secret-types","pushed_at":"2026-10-25T21:13:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/self-destructing-git-garbage","pushed_at":"2026-10-14T01:41:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/session-sentinel","pushed_at":"2026-10-20T13:17:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/sholes","pushed_at":"2026-10-18T13:40:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/sinople-theme","pushed_at":"2026-10-21T15:52:54Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/smtp-notify-action","pushed_at":"2026-10-24T08:43:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/snapcreate","pushed_at":"2026-10-23T00:35:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/snifs","pushed_at":"2026-10-01T19:46:36Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/social-media-polygraph","pushed_at":"2026-10-18T03:54:15Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/social-media-tools","pushed_at":"2026-10-11T17:34:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/somethings-fishy","pushed_at":"2026-10-23T08:16:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/squeakwell","pushed_at":"2026-10-23T07:06:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/squisher-corpus","pushed_at":"2026-10-01T19:46:07Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/ssg-collection","pushed_at":"2026-10-07T11:09:52Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/stateful-artefacts","pushed_at":"2026-10-25T09:14:09Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/statistikles","pushed_at":"2026-10-23T13:46:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/supernorma","pushed_at":"2026-10-22T05:55:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/system-et","pushed_at":"2026-10-23T07:14:25Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/tangle","pushed_at":"2026-10-13T06:09:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/technical-notes","pushed_at":"2026-10-01T19:46:46Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/tentacles-agentic-syllabus","pushed_at":"2026-10-01T19:41:13Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/the-metadatastician","pushed_at":"2026-10-13T15:56:33Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/this-ssg","pushed_at":"2026-10-01T06:00:53Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/thunderbird-template-reloaded","pushed_at":"2026-10-19T20:21:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/tlaiser","pushed_at":"2026-10-23T00:50:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/tools","pushed_at":"2026-10-08T12:09:59Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/tree-navigator","pushed_at":"2026-10-22T12:21:10Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/trigger","pushed_at":"2026-10-08T17:50:35Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/trope-checker","pushed_at":"2026-10-19T20:16:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/trope-particularity-workbench","pushed_at":"2026-10-06T17:01:47Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/tropical-types","pushed_at":"2026-10-12T21:12:08Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/twingate-helm-deploy","pushed_at":"2026-10-26T07:33:21Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/typed-wasm","pushed_at":"2026-10-17T10:15:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/typedqliser","pushed_at":"2026-10-23T00:50:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/typefix-zero","pushed_at":"2026-10-01T19:42:04Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/typell","pushed_at":"2026-10-25T08:25:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/ubicity","pushed_at":"2026-10-23T17:57:22Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/unified-api-adapter","pushed_at":"2026-10-18T07:57:05Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/unified-dataset-vocab","pushed_at":"2026-10-23T21:38:41Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/universal-chat-extractor","pushed_at":"2026-10-26T14:31:53Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/universal-extension-format","pushed_at":"2026-10-21T14:34:50Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/universal-language-server-plugin","pushed_at":"2026-10-23T21:36:19Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/universal-project-manager","pushed_at":"2026-10-01T19:38:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/valence-shell","pushed_at":"2026-10-25T15:46:40Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/vcl-ut","pushed_at":"2026-10-24T11:37:20Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/vcs-ircd","pushed_at":"2026-10-24T20:51:11Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/veridical-simulation-core","pushed_at":"2026-10-01T15:28:02Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/verisimdb","pushed_at":"2026-10-25T22:35:43Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/verisimdb-data","pushed_at":"2026-10-17T18:44:55Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/verisimiser","pushed_at":"2026-10-25T22:17:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/vex-tools","pushed_at":"2026-10-08T17:33:13Z","visibility":"private"}
+{"fork":false,"full_name":"hyperpolymath/vexometer","pushed_at":"2026-10-26T15:21:48Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/vext","pushed_at":"2026-10-17T02:25:06Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/vocarium","pushed_at":"2026-10-23T21:12:07Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/volumod","pushed_at":"2026-10-26T07:34:20Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/voyage-enterprise-decision-system","pushed_at":"2026-10-24T11:20:00Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/wokelang","pushed_at":"2026-10-26T07:33:45Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/wokelangiser","pushed_at":"2026-10-23T07:52:17Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/wordpress-tools","pushed_at":"2026-10-13T15:25:28Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/wsl-compute-governor-dispatcher","pushed_at":"2026-10-22T06:54:54Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/xmlpull-zig","pushed_at":"2026-10-20T22:33:12Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zerostep","pushed_at":"2026-10-20T22:20:57Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zerotier-k8s-link","pushed_at":"2026-10-01T19:35:18Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zig-boringtls","pushed_at":"2026-10-20T22:24:01Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zig-dnssec","pushed_at":"2026-10-20T22:35:05Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zig-icu-collation","pushed_at":"2026-10-20T22:28:26Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zig-unorm","pushed_at":"2026-10-20T22:47:54Z","visibility":"public"}
+{"fork":false,"full_name":"hyperpolymath/zotero-tools","pushed_at":"2026-10-26T01:17:04Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/.github","pushed_at":"2026-10-12T22:05:23Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/MetaManifold-Evidence","pushed_at":"2026-10-23T00:25:20Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/ZenodoDeposits.jl","pushed_at":"2026-10-23T08:00:12Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/ZeroInflatedCounts.jl","pushed_at":"2026-10-23T13:46:54Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/_pathroot","pushed_at":"2026-10-25T09:37:44Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/affinescript-libraries","pushed_at":"2026-10-19T22:40:39Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/authority-watch","pushed_at":"2026-10-16T05:24:49Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/berry-blocks","pushed_at":"2026-10-21T22:26:22Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/berrywiki","pushed_at":"2026-10-23T07:02:15Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/berrywiki-course-template","pushed_at":"2026-10-18T17:05:28Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/bowtie-workbench","pushed_at":"2026-10-23T22:19:45Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/burble","pushed_at":"2026-10-26T07:34:12Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/cadastra","pushed_at":"2026-10-22T18:10:14Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/cerro-torre","pushed_at":"2026-10-24T05:31:14Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/cleave","pushed_at":"2026-10-21T14:34:17Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/common-signal","pushed_at":"2026-10-26T05:59:41Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/consent-aware-web","pushed_at":"2026-10-16T20:05:13Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/first-post","pushed_at":"2026-10-22T21:09:24Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/gossamer","pushed_at":"2026-10-26T00:02:32Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/groove","pushed_at":"2026-10-22T09:26:55Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/hvn-dehallucinator","pushed_at":"2026-10-20T13:21:14Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/insolvency-tycoon","pushed_at":"2026-10-13T22:38:04Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/knot-knot","pushed_at":"2026-10-23T01:29:47Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/kyq","pushed_at":"2026-10-25T22:11:29Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/large-language-michelangelo","pushed_at":"2026-10-01T19:37:55Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/lintel","pushed_at":"2026-10-19T09:35:21Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/marid","pushed_at":"2026-10-23T21:36:14Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/metadatastician-governance","pushed_at":"2026-10-19T18:49:35Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/odraz","pushed_at":"2026-10-15T21:59:43Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/paint-type","pushed_at":"2026-10-23T16:48:06Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/phi-LAM","pushed_at":"2026-10-01T14:05:44Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/progblocks","pushed_at":"2026-10-22T13:55:19Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/proglanging-languages","pushed_at":"2026-10-26T06:28:47Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/rokur","pushed_at":"2026-10-18T13:24:54Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/selur","pushed_at":"2026-10-25T07:53:10Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/sim-public-relations","pushed_at":"2026-10-22T14:07:34Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/spline","pushed_at":"2026-10-21T17:20:19Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/standard-operating-psychopathy","pushed_at":"2026-10-18T17:21:16Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/standards","pushed_at":"2026-10-26T16:44:26Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/stapeln","pushed_at":"2026-10-25T08:03:20Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/svalinn","pushed_at":"2026-10-24T15:41:48Z","visibility":"public"}
+{"fork":false,"full_name":"metadatastician/vordr","pushed_at":"2026-10-24T21:38:46Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-agda","pushed_at":"2026-10-01T12:42:34Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-coq","pushed_at":"2026-10-01T20:10:43Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-fsharp","pushed_at":"2026-10-01T12:40:11Z","visibility":"public"}
+{"fork":true,"full_name":"stuff-of-awe/awesome-gleam","pushed_at":"2026-09-21T12:07:36Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-haskell","pushed_at":"2026-10-04T01:33:38Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-idris2","pushed_at":"2026-10-22T16:27:35Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-ipfs","pushed_at":"2026-10-01T12:39:15Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-nickel","pushed_at":"2026-10-12T19:53:02Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-ocaml","pushed_at":"2026-10-01T13:34:47Z","visibility":"public"}
+{"fork":false,"full_name":"stuff-of-awe/awesome-provable","pushed_at":"2026-10-01T14:00:19Z","visibility":"public"}
+{"fork":true,"full_name":"stuff-of-awe/awesome-zig","pushed_at":"2026-10-01T22:58:21Z","visibility":"public"}
diff --git a/docs/catalogue/census/template-paths.txt b/docs/catalogue/census/template-paths.txt
new file mode 100644
index 00000000..34b3e1aa
--- /dev/null
+++ b/docs/catalogue/census/template-paths.txt
@@ -0,0 +1,16 @@
+.machine_readable/coaptation/core/Coaptation.idr
+src/interface/Abi/Foreign.idr
+src/interface/Abi/Layout.idr
+src/interface/Abi/Types.idr
+src/interface/abi.ipkg
+verification/proofs/agda/Properties.agda
+verification/proofs/coq/TypeSafety.v
+verification/proofs/idris2/ABI/Compliance.idr
+verification/proofs/idris2/ABI/Foreign.idr
+verification/proofs/idris2/ABI/Layout.idr
+verification/proofs/idris2/ABI/Platform.idr
+verification/proofs/idris2/ABI/Pointers.idr
+verification/proofs/idris2/Types.idr
+verification/proofs/lean4/ApiTypes.lean
+verification/proofs/lean4/lean-toolchain
+verification/proofs/tlaplus/StateMachine.tla
diff --git a/docs/catalogue/census/unreachable.jsonl b/docs/catalogue/census/unreachable.jsonl
new file mode 100644
index 00000000..54cc9dfa
--- /dev/null
+++ b/docs/catalogue/census/unreachable.jsonl
@@ -0,0 +1,37 @@
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"catachresis-colloquium/reflexive-ai-studio"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/007-lang"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/HOL"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/achievements-lab"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/ai-cli-lab"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/axel-protocol"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/blog-drafts"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/claude-config-vault"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/claude-memory"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/contractiles-a2-lab"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/cut-calculus"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dev-notes-vault"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dev-notes"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dotfiles"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/echobox"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/email-octad-experiment"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/estate-scripts"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/frayed-knot-toolkit"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/fumble"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/git-seo"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/hottchpotch"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/hyperpolymath-sovereign-registry"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/info"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/jewell.nexus"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/jonathanjewell.dev"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/lcb-website"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/lfs-shared"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/linguist"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/memory-vault"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/poly-observability-mcp"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/polystack"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/rescript"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/squisher-corpus"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/this-ssg"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/tools"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/typefix-zero"}
+{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/vex-tools"}
diff --git a/scripts/census/build-rows.sh b/scripts/census/build-rows.sh
new file mode 100644
index 00000000..8dc54ae0
--- /dev/null
+++ b/scripts/census/build-rows.sh
@@ -0,0 +1,64 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Fold the raw, path-level census into one row per repository.
+#
+# Usage: build-rows.sh RAW_DIR TEMPLATE_PATHS > catalogue-rows.jsonl
+#   RAW_DIR         files.jsonl, holes.jsonl, decls.jsonl, repos-with-status.jsonl
+#                   (written by census-repo.sh + summarise.sh; not committed)
+#   TEMPLATE_PATHS  one path per line: proof files the RSR template ships,
+#                   which are boilerplate wherever they appear
+#
+# Rows carry counts only, never file paths, so the committed data neither
+# grows with the estate's file trees nor repeats other repositories' paths.
+# A repo's "own" files are those not on the template list; files under
+# tests/, fixtures/, corpus/, benches/ count as fixtures. "theory" is a
+# first-pass heuristic: more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK
+# files. A human confirms each row.
+set -euo pipefail
+R=$1 T=$2
+tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT
+
+jq -r '[.repo,.path,.ext]|@tsv' "$R/files.jsonl" \
+| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t)' "$T" - \
+| awk -F'\t' 'BEGIN{OFS="\t"} {
+    e=$3; p="other"
+    if (e ~ /agda/) p="agda"; else if (e ~ /idr|ipkg/) p="idris2"
+    else if (e ~ /lean|lakefile/) p="lean"; else if (e == "v" || e ~ /CoqProject/) p="rocq"
+    else if (e == "thy") p="isabelle"; else if (e == "tla" || e == "cfg") p="tla"
+    else if (e == "dk" || e == "lp") p="dedukti"; else if (e ~ /smt2|tptp/ || e == "p") p="smt-atp"
+    else if (e ~ /ad[sb]/) p="spark"; else if (e == "mlw") p="why3"
+    else if (e == "fst") p="fstar"; else if (e == "dfy") p="dafny"; else if (e == "als") p="alloy"
+    fx = ($2 ~ /(^|\/)(tests?|fixtures?|corpus|corpus_fixtures|benches|benchmarks?)\//) ? 1 : 0
+    print $1, p, fx }' > "$tmp/cls.tsv"
+
+jq -r '[.repo,.file,.class]|@tsv' "$R/holes.jsonl" \
+| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1"\t"$3}' "$T" - > "$tmp/holes.tsv"
+
+jq -r '[.repo,.file]|@tsv' "$R/decls.jsonl" \
+| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1}' "$T" - > "$tmp/decls.tsv"
+
+jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv"
+
+awk -F'\t' '
+  FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }
+  FILENAME ~ /decls\.tsv$/  { d[$1]++; next }
+  FILENAME ~ /status\.tsv$/ { if (!($1 in st)) st[$1]=$2; next }
+  { n[$1]++; if ($3) fx[$1]++; pc[$1" "$2]++
+    if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark/) en[$1]++ }
+  END {
+    split("agda lean rocq isabelle idris2 spark tla dedukti smt-atp why3 fstar dafny alloy other", L, " ")
+    for (r in n) {
+      provers=""
+      for (i=1;i<=14;i++) if (pc[r" "L[i]]) provers = provers L[i] " " pc[r" "L[i]] ", "
+      sub(/, $/, "", provers)
+      printf "%s\t%s\t%d\t%d\t%s\t%d\t%d\t%d\t%d\t%d\t%s\n",
+        (th[r]+0 > en[r]+0) ? "theory" : "engineering", r, n[r], fx[r]+0, provers,
+        d[r]+0, h[r" hole"]+0, h[r" axiom"]+0, h[r" unsafe"]+0, h[r" policy"]+0,
+        (r in st) ? st[r] : ""
+    }
+  }' "$tmp/holes.tsv" "$tmp/decls.tsv" "$tmp/status.tsv" "$tmp/cls.tsv" \
+| sort -t$'\t' -k2,2 \
+| jq -RcS 'split("\t") | {class:.[0], repo:.[1], own_files:(.[2]|tonumber),
+    fixture_files:(.[3]|tonumber), provers:.[4], declarations:(.[5]|tonumber),
+    holes:(.[6]|tonumber), axioms:(.[7]|tonumber), unsafe:(.[8]|tonumber),
+    policy:(.[9]|tonumber), status_doc:.[10]}'
diff --git a/scripts/census/census-repo.sh b/scripts/census/census-repo.sh
new file mode 100755
index 00000000..c5fdc637
--- /dev/null
+++ b/scripts/census/census-repo.sh
@@ -0,0 +1,199 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Usage: census-repo.sh OWNER/REPO   (run with cwd-independent absolute paths)
+# Writes per-repo outputs into $BASE/out/<owner>__<repo>.{files,decls,holes,agdaopts,status,unreach}.jsonl
+set -uo pipefail
+FN=$1
+BASE=${MATHESIS_DATA:?set MATHESIS_DATA to the census work directory}
+HOLES=$(cd "$(dirname "$0")" && pwd)/proof-holes.sh
+KEY=${FN/\//__}
+D=$BASE/clones/$KEY
+O=$BASE/out/$KEY
+mkdir -p "$BASE/out"
+rm -rf "$D" "$O".*
+
+clone() { timeout 600 git clone -q --depth 1 --filter=blob:none --no-checkout "https://github.com/$FN" "$D" 2>&1; }
+err=$(clone); rc=$?
+if [ $rc -ne 0 ]; then
+  rm -rf "$D"; sleep 2; err=$(clone); rc=$?
+fi
+if [ $rc -ne 0 ]; then
+  jq -cnS --arg r "$FN" --arg e "$(printf '%s' "$err" | tr '\n' ' ' | cut -c1-300)" --argjson rc $rc '{repo:$r,error:$e,exit:$rc}' > "$O.unreach.jsonl"
+  rm -rf "$D"; exit 0
+fi
+
+git -C "$D" ls-tree -r --name-only HEAD > "$O.tree" 2>/dev/null || true
+if ! [ -s "$O.tree" ]; then rm -rf "$D" "$O.tree"; exit 0; fi
+
+# proof-status docs
+grep -iE '(^|/)(PROOF-STATUS[^/]*|PROOF-NEEDS[^/]*|proof-debt[^/]*)$' "$O.tree" \
+  | jq -RcS --arg r "$FN" '{path:., repo:$r}' > "$O.status.jsonl"
+
+# candidate paths
+grep -E '\.(agda|lagda|lagda\.md|idr|lidr|ipkg|lean|v|thy|tla|cfg|dk|lp|smt2|tptp|p|ads|adb|mlw|fst|dfy|als|gpr)$|(^|/)(\.?lean-toolchain|lakefile\.lean|lakefile\.toml|_CoqProject|dune|dune-project)$|\.agda-lib$' "$O.tree" > "$O.cand"
+if ! [ -s "$O.cand" ]; then rm -rf "$D"; rm -f "$O.tree" "$O.cand"; [ -s "$O.status.jsonl" ] || rm -f "$O.status.jsonl"; exit 0; fi
+
+# .cfg only if a .tla sits in the same directory; dune only if .v exists
+grep -E '\.tla$' "$O.cand" | sed -E 's#[^/]*$##' | sort -u > "$O.tladirs"
+grep -qE '\.v$' "$O.cand" && HASV=1 || HASV=0
+: > "$O.co"
+while IFS= read -r p; do
+  case "$p" in
+    *.cfg) dir=${p%"${p##*/}"}; grep -qxF -- "$dir" "$O.tladirs" && echo "$p" >> "$O.co" ;;
+    dune|*/dune|dune-project|*/dune-project) [ $HASV = 1 ] && echo "$p" >> "$O.co" ;;
+    *) echo "$p" >> "$O.co" ;;
+  esac
+done < "$O.cand"
+
+if [ -s "$O.co" ]; then
+  tr '\n' '\0' < "$O.co" | (cd "$D" && timeout 1800 xargs -0 -n 400 git checkout -q HEAD -- >/dev/null 2>&1)
+fi
+
+# Rocq repo-level gate
+ROCQ=0
+if grep -qE '(^|/)_CoqProject$' "$O.cand"; then ROCQ=1; fi
+if [ $ROCQ = 0 ] && [ $HASV = 1 ]; then
+  while IFS= read -r p; do
+    case "$p" in dune|*/dune|dune-project|*/dune-project) grep -qiE '\(coq|\(rocq' "$D/$p" 2>/dev/null && ROCQ=1 ;; esac
+  done < "$O.co"
+  if [ $ROCQ = 0 ]; then
+    while IFS= read -r p; do
+      grep -qE '(Require|Theorem)' "$D/$p" 2>/dev/null && { ROCQ=1; break; }
+    done < <(grep -E '\.v$' "$O.co")
+  fi
+fi
+# SPARK repo-level gate
+SPARK=0
+grep -qE '\.gpr$' "$O.cand" && SPARK=1
+if [ $SPARK = 0 ]; then
+  while IFS= read -r p; do grep -qi 'SPARK_Mode' "$D/$p" 2>/dev/null && { SPARK=1; break; }; done < <(grep -E '\.(ads|adb)$' "$O.co")
+fi
+
+prover_of() {
+  case "$1" in
+    *.agda|*.lagda|*.lagda.md|*.agda-lib) echo agda ;;
+    *.idr|*.lidr|*.ipkg) echo idris2 ;;
+    *.lean|*lean-toolchain|*lakefile.lean|*lakefile.toml) echo lean ;;
+    *.v|*_CoqProject) echo rocq ;;
+    *.thy) echo isabelle ;;
+    *.tla|*.cfg) echo tla ;;
+    *.dk) echo dedukti ;;
+    *.lp) echo lambdapi ;;
+    *.smt2) echo smtlib ;;
+    *.tptp|*.p) echo tptp ;;
+    *.ads|*.adb|*.gpr) echo spark ;;
+    *.mlw) echo why3 ;;
+    *.fst) echo fstar ;;
+    *.dfy) echo dafny ;;
+    *.als) echo alloy ;;
+  esac
+}
+ext_of() {
+  local b=${1##*/}
+  case "$b" in
+    *.lagda.md) echo lagda.md ;;
+    lean-toolchain|.lean-toolchain|lakefile.lean|lakefile.toml|_CoqProject) echo "$b" ;;
+    *.agda-lib) echo agda-lib ;;
+    *.*) echo "${b##*.}" ;;
+    *) echo "$b" ;;
+  esac
+}
+
+: > "$O.keep"
+while IFS= read -r p; do
+  f=$D/$p
+  case "$p" in
+    dune|*/dune|dune-project|*/dune-project) continue ;;
+    *.v)
+      [ $ROCQ = 1 ] || continue
+      # skip obvious Verilog
+      if grep -qE '^\s*endmodule' "$f" 2>/dev/null && ! grep -qE '^\s*(Require|From|Theorem|Lemma|Definition|Inductive)' "$f"; then continue; fi ;;
+    *.ads|*.adb|*.gpr) [ $SPARK = 1 ] || continue ;;
+    *.p) grep -qE '^\s*(fof|cnf|tff|thf|include)\(' "$f" 2>/dev/null || continue ;;
+    *.lp) grep -qE '^\s*(symbol|require|rule|constant|injective|opaque)\b' "$f" 2>/dev/null || continue ;;
+  esac
+  echo "$p" >> "$O.keep"
+done < "$O.co"
+
+while IFS= read -r p; do
+  jq -cnS --arg e "$(ext_of "$p")" --arg p "$p" --arg r "$FN" '{ext:$e,path:$p,repo:$r}'
+done < "$O.keep" > "$O.files.jsonl"
+
+# declarations: emit TSV prover\tkind\tline\tname\tfile then convert
+: > "$O.decl.tsv"
+while IFS= read -r p; do
+  f=$D/$p; pr=$(prover_of "$p")
+  [ -f "$f" ] || continue
+  case "$p" in
+    *.lean)
+      grep -nE '^\s*((private|protected|noncomputable|partial|unsafe|@\[[^]]*\])\s+)*(theorem|lemma|def|structure|inductive|axiom)\s+[^ :({\[]+' "$f" \
+      | sed -E 's/^([0-9]+):\s*((private|protected|noncomputable|partial|unsafe|@\[[^]]*\])\s+)*(theorem|lemma|def|structure|inductive|axiom)\s+([^ :({[]+).*/\1\t\4\t\5/' \
+      | awk -F'\t' -v pr=lean -v fl="$p" 'NF==3{print pr"\t"$2"\t"$1"\t"$3"\t"fl}' ;;
+    *.v)
+      grep -nE '^\s*(Theorem|Lemma|Corollary|Proposition|Fact|Remark|Definition|Fixpoint|Inductive|Axiom|Parameter)\s+[^ :({]+' "$f" \
+      | sed -E 's/^([0-9]+):\s*(Theorem|Lemma|Corollary|Proposition|Fact|Remark|Definition|Fixpoint|Inductive|Axiom|Parameter)\s+([^ :({.]+).*/\1\t\2\t\3/' \
+      | awk -F'\t' -v pr=rocq -v fl="$p" 'NF==3{print pr"\t"$2"\t"$1"\t"$3"\t"fl}' ;;
+    *.thy)
+      grep -nE '^\s*(theorem|lemma|corollary|definition|fun|datatype|axiomatization)\s+[^ :]+' "$f" \
+      | sed -E 's/^([0-9]+):\s*(theorem|lemma|corollary|definition|fun|datatype|axiomatization)\s+("?[^ :"]+"?).*/\1\t\2\t\3/' \
+      | awk -F'\t' -v pr=isabelle -v fl="$p" 'NF==3{gsub(/"/,"",$3); print pr"\t"$2"\t"$1"\t"$3"\t"fl}' ;;
+    *.agda|*.lagda|*.lagda.md)
+      awk -v fl="$p" -v lit=$([[ "$p" == *.lagda* ]] && echo 1 || echo 0) '
+        BEGIN{code = lit ? 0 : 1; post=0}
+        {
+          line=$0
+          if (lit) {
+            if (line ~ /^\\begin\{code\}/ || line ~ /^```/) { if (line ~ /^```/) code = !code; else code=1; next }
+            if (line ~ /^\\end\{code\}/) { code=0; next }
+            if (!code) next
+          }
+          if (post && line ~ /^[ \t]+[^ \t-][^ \t]*([ \t]+[^ \t:][^ \t]*)*[ \t]+:([ \t]|$)/) {
+            s=line; sub(/^[ \t]+/,"",s); n=split(s,a,/[ \t]+/); for(i=1;i<=n && a[i]!=":";i++) print "agda\tpostulate\t" NR "\t" a[i] "\t" fl; next }
+          if (line ~ /^[^ \t]/) post=0
+          if (line ~ /^postulate[ \t]+[^ \t]/) { s=line; sub(/^postulate[ \t]+/,"",s); n=split(s,a,/[ \t]+/); for(i=1;i<=n && a[i]!=":";i++) print "agda\tpostulate\t" NR "\t" a[i] "\t" fl }
+          if (line ~ /^postulate([ \t]|$)/) { post=1; print "agda\tpostulate-block\t" NR "\tpostulate\t" fl; next }
+          if (line ~ /^(data|record)[ \t]+[^ \t]+/) { split(line,a,/[ \t]+/); print "agda\t" a[1] "\t" NR "\t" a[2] "\t" fl; next }
+          if (line ~ /^(module|open|import|infix|infixl|infixr|private|abstract|instance|mutual|variable|syntax|pattern|--|\{-)/) next
+          if (line ~ /^[^ \t:][^ \t]*([ \t]+[^ \t:][^ \t]*)*[ \t]+:([ \t]|$)/) { split(line,a,/[ \t]+/); print "agda\tsig\t" NR "\t" a[1] "\t" fl }
+        }' "$f" ;;
+    *.idr)
+      awk -v fl="$p" '
+        /^(module|import|namespace|%|--|\|\|\||infix|infixl|infixr|prefix|mutual|parameters|using)/ {next}
+        /^((public[ \t]+)?export[ \t]+|private[ \t]+)?(data|record|interface)[ \t]+[^ \t]+/ {
+          s=$0; sub(/^((public[ \t]+)?export[ \t]+|private[ \t]+)/,"",s); split(s,a,/[ \t]+/); print "idris2\t" a[1] "\t" NR "\t" a[2] "\t" fl; next }
+        /^((public[ \t]+)?export[ \t]+|private[ \t]+|total[ \t]+|partial[ \t]+|covering[ \t]+)*[^ \t:(][^ \t]*[ \t]+:([ \t]|$)/ {
+          s=$0; while (s ~ /^(public|export|private|total|partial|covering)[ \t]+/) sub(/^[^ \t]+[ \t]+/,"",s); split(s,a,/[ \t]+/); print "idris2\tsig\t" NR "\t" a[1] "\t" fl }' "$f" ;;
+    *.tla)
+      grep -nE '^\s*(THEOREM|LEMMA)\s+[A-Za-z_][A-Za-z0-9_]*\s*==' "$f" \
+      | sed -E 's/^([0-9]+):\s*(THEOREM|LEMMA)\s+([A-Za-z0-9_]+).*/\1\t\2\t\3/' \
+      | awk -F'\t' -v fl="$p" 'NF==3{print "tla\t"$2"\t"$1"\t"$3"\t"fl}' ;;
+    *.cfg)
+      awk -v fl="$p" '
+        /^[ \t]*(INVARIANT|INVARIANTS|PROPERTY|PROPERTIES)([ \t]|$)/ { mode=$1; for(i=2;i<=NF;i++) if ($i ~ /^[A-Za-z_]/) print "tla\t" mode "\t" NR "\t" $i "\t" fl; next }
+        /^[ \t]*[A-Z]+([ \t]|$)/ && $1 ~ /^(CONSTANT|CONSTANTS|INIT|NEXT|SPECIFICATION|SYMMETRY|VIEW|CONSTRAINT|ACTION_CONSTRAINT|CHECK_DEADLOCK|ALIAS|POSTCONDITION)$/ { mode=""; next }
+        mode!="" && /^[ \t]+[A-Za-z_][A-Za-z0-9_]*[ \t]*$/ { s=$0; gsub(/[ \t]/,"",s); print "tla\t" mode "\t" NR "\t" s "\t" fl }' "$f" ;;
+  esac
+done < "$O.keep" >> "$O.decl.tsv"
+awk -F'\t' 'NF==5' "$O.decl.tsv" | jq -RcS --arg r "$FN" 'split("\t") | {prover:.[0],kind:.[1],line:(.[2]|tonumber),name:.[3],file:.[4],repo:$r}' > "$O.decls.jsonl"
+
+# Agda OPTIONS pragmas
+while IFS= read -r p; do
+  case "$p" in
+    *.agda|*.lagda|*.lagda.md)
+      opts=$(grep -oE '\{-#\s*OPTIONS[^#]*#-\}' "$D/$p" 2>/dev/null | sed -E 's/\{-#\s*OPTIONS\s*//; s/\s*#-\}//' | tr '\n' ' ' | sed 's/ *$//')
+      jq -cnS --arg f "$p" --arg o "$opts" --arg r "$FN" '{file:$f,options:$o,repo:$r,safe:($o|test("--safe"))}' ;;
+    *.agda-lib)
+      fl=$(grep -E '^\s*flags\s*:' "$D/$p" 2>/dev/null | sed -E 's/^\s*flags\s*:\s*//' | tr '\n' ' ' | sed 's/ *$//')
+      jq -cnS --arg f "$p" --arg o "$fl" --arg r "$FN" '{file:$f,lib_flags:$o,repo:$r,safe:($o|test("--safe"))}' ;;
+  esac
+done < "$O.keep" > "$O.agdaopts.jsonl"
+
+# holes (only if any kept proof file)
+if [ -s "$O.keep" ]; then
+  timeout 1800 bash "$HOLES" --fail-on none "$D" 2>/dev/null | jq -cS --arg r "$FN" '. + {repo:$r}' > "$O.holes.jsonl"
+fi
+
+rm -rf "$D"
+rm -f "$O.tree" "$O.cand" "$O.co" "$O.tladirs" "$O.decl.tsv" "$O.keep"
+for x in "$O".*; do [ -s "$x" ] || rm -f "$x"; done
+exit 0
diff --git a/scripts/census/proof-holes.sh b/scripts/census/proof-holes.sh
new file mode 100644
index 00000000..2e7c7065
--- /dev/null
+++ b/scripts/census/proof-holes.sh
@@ -0,0 +1,123 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# proof-craft: inventory proof escape hatches in a tree.
+#
+# Usage: proof-holes.sh [--fail-on hole|axiom|any|none] [--summary] [--exclude DIRNAME]... [DIR]
+#
+# Prints one JSON object per finding (keys sorted, one per line):
+#   {"class":…,"file":…,"lang":…,"line":N,"marker":…,"text":…}
+# class is one of
+#   hole    an unfinished proof (sorry, Admitted, ?hole, believe_me, …)  -> OWED
+#   axiom   trusted base grows (postulate, Axiom, #[trusted], pragma Assume, …)
+#   unsafe  a checker is switched off (TERMINATING, Unset Guard Checking, SPARK_Mode Off, …)
+#   policy  estate rule broken (import Mathlib, Agda file without --safe)
+#
+# This is a textual scan: it finds candidates, it does not decide them. A
+# kernel-level audit (#print axioms, Print Assumptions, gnatprove report,
+# agda --safe) is the authority; see references/ledger.md. Whole-line comments
+# are skipped; markers inside block comments or strings may still be reported.
+#
+# Exit: 0 clean at the chosen --fail-on level (default: hole), 1 otherwise,
+# 2 usage error.
+set -uo pipefail
+
+FAIL_ON=hole SUMMARY=0 DIR=. EXTRA_EX=()
+while [ $# -gt 0 ]; do
+  case "$1" in
+    --fail-on) FAIL_ON=${2:-}; shift 2 ;;
+    --summary) SUMMARY=1; shift ;;
+    --exclude) EXTRA_EX+=("$2"); shift 2 ;;
+    -h|--help) sed -n '3,22p' "$0"; exit 0 ;;
+    -*) echo "unknown option: $1" >&2; exit 2 ;;
+    *) DIR=$1; shift ;;
+  esac
+done
+case "$FAIL_ON" in hole|axiom|any|none) ;; *) echo "--fail-on must be hole|axiom|any|none" >&2; exit 2 ;; esac
+command -v jq >/dev/null || { echo "jq is required" >&2; exit 2; }
+
+EXCLUDE=(--exclude-dir=.git --exclude-dir=target --exclude-dir=_build --exclude-dir=build
+         --exclude-dir=.lake --exclude-dir=node_modules --exclude-dir=deps --exclude-dir=vendor)
+for d in "${EXTRA_EX[@]}"; do EXCLUDE+=(--exclude-dir="$d"); done
+
+# rule: lang~include-globs~comment-regex~class~marker~PCRE
+RULES=$(cat <<'EOF'
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~axiom~postulate~^\s*postulate\b
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~hole~{! !}~\{!
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~unsafe~TERMINATING~\{-#\s*(NON_)?TERMINATING\s*#-\}
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~unsafe~NO_POSITIVITY_CHECK~\{-#\s*NO_POSITIVITY_CHECK
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~unsafe~NO_UNIVERSE_CHECK~\{-#\s*NO_UNIVERSE_CHECK
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~unsafe~--type-in-type~--type-in-type
+agda~*.agda,*.lagda,*.lagda.md~^\s*--~axiom~primTrustMe~\bprimTrustMe\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~hole~believe_me~\bbelieve_me\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~hole~assert_total~\bassert_total\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~hole~assert_smaller~\bassert_smaller\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~hole~idris_crash~\bidris_crash\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~hole~?hole~(^|[\s(=])\?[a-z_][A-Za-z0-9_']*
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~unsafe~%default partial~%default\s+partial
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~unsafe~partial~^\s*partial\b
+idris2~*.idr,*.lidr~^\s*(--|\|\|\|)~axiom~unsafePerformIO~\bunsafePerformIO\b
+lean~*.lean~^\s*--~hole~sorry~\bsorry\b
+lean~*.lean~^\s*--~hole~admit~\badmit\b
+lean~*.lean~^\s*--~axiom~axiom~^\s*(private\s+|protected\s+)?axiom\b
+lean~*.lean~^\s*--~axiom~native_decide~\bnative_decide\b
+lean~*.lean~^\s*--~axiom~implemented_by~@\[implemented_by
+lean~*.lean~^\s*--~unsafe~unsafe~^\s*(private\s+)?unsafe\b
+lean~*.lean~^\s*--~policy~import Mathlib~^\s*import\s+Mathlib
+rocq~*.v~^\s*\(\*~hole~Admitted~\bAdmitted\.
+rocq~*.v~^\s*\(\*~hole~admit~\badmit\.
+rocq~*.v~^\s*\(\*~hole~give_up~\bgive_up\b
+rocq~*.v~^\s*\(\*~axiom~Axiom~^\s*(Axiom|Axioms|Conjecture|Parameter|Parameters)\b
+rocq~*.v~^\s*\(\*~unsafe~Unset Checking~Unset\s+(Guard|Positivity|Universe)\s+Checking
+rocq~*.v~^\s*\(\*~unsafe~bypass_check~#\[\s*bypass_check
+isabelle~*.thy~^\s*\(\*~hole~sorry~\bsorry\b
+isabelle~*.thy~^\s*\(\*~hole~oops~\boops\b
+isabelle~*.thy~^\s*\(\*~axiom~axiomatization~\baxiomatization\b
+isabelle~*.thy~^\s*\(\*~unsafe~quick_and_dirty~quick_and_dirty
+creusot~*.rs~^\s*//~axiom~#[trusted]~#\[\s*(creusot::)?trusted\s*\]
+creusot~*.rs~^\s*//~hole~assume!~\b(proof_)?assume!\s*\(
+spark~*.adb,*.ads~^\s*--~hole~pragma Assume~pragma\s+Assume\b
+spark~*.adb,*.ads~^\s*--~unsafe~SPARK_Mode Off~SPARK_Mode\s*(=>\s*)?\(?\s*Off
+spark~*.adb,*.ads~^\s*--~unsafe~Skip_Proof~Skip_(Flow_And_)?Proof
+spark~*.adb,*.ads~^\s*--~axiom~Annotate False_Positive~Annotate\s*\(\s*GNATprove\s*,\s*(False_Positive|Intentional)
+dedukti~*.dk,*.lp~^\s*(//|\(;)~hole~admit~\badmit(ted)?\b
+EOF
+)
+
+emit() { # lang class marker file line text
+  jq -cnS --arg lang "$1" --arg class "$2" --arg marker "$3" --arg file "$4" \
+        --argjson line "$5" --arg text "$6" \
+        '{lang:$lang,class:$class,marker:$marker,file:$file,line:$line,text:$text}'
+}
+
+OUT=$(mktemp); trap 'rm -f "$OUT"' EXIT
+while IFS='~' read -r lang globs comment class marker re; do
+  [ -z "$lang" ] && continue
+  inc=(); IFS=',' read -ra gl <<<"$globs"; for g in "${gl[@]}"; do inc+=(--include="$g"); done
+  # Rocq shares .v with V and Verilog; only scan .v files that look like Rocq.
+  grep -rnPI "${EXCLUDE[@]}" "${inc[@]}" -e "$re" "$DIR" 2>/dev/null | while IFS= read -r hit; do
+    f=${hit%%:*}; rest=${hit#*:}; n=${rest%%:*}; txt=${rest#*:}
+    printf '%s\n' "$txt" | grep -qP -- "$comment" && continue
+    if [ "$lang" = rocq ] && ! grep -qE '^\s*(Require|From|Theorem|Lemma|Definition|Inductive|Proof\.)' "$f"; then continue; fi
+    if [ "$lang" = creusot ] && ! grep -qE 'creusot|pearlite|#\[\s*(requires|ensures)' "$f"; then continue; fi
+    emit "$lang" "$class" "$marker" "${f#"$DIR"/}" "$n" "$(printf '%s' "$txt" | sed 's/^\s*//' | cut -c1-200)"
+  done >>"$OUT"
+done <<<"$RULES"
+
+# Agda: every non-fixture module should be checked under --safe.
+while IFS= read -r f; do
+  grep -qE 'OPTIONS[^#]*--safe' "$f" || emit agda policy "no --safe" "${f#"$DIR"/}" 1 "file does not set {-# OPTIONS --safe #-}" >>"$OUT"
+done < <(find "$DIR" \( -name .git -o -name _build -o -name build -o -name target $(for d in "${EXTRA_EX[@]}"; do printf -- "-o -name %s " "$d"; done)\) -prune -o -type f -name '*.agda' -print 2>/dev/null)
+
+sort -u "$OUT"
+
+if [ "$SUMMARY" = 1 ]; then
+  jq -rs 'group_by(.lang+" "+.class) | map("\(.[0].lang) \(.[0].class): \(length)") | .[]' "$OUT" >&2
+fi
+
+count() { jq -s --arg c "$1" '[.[] | select($c=="any" or .class==$c)] | length' "$OUT"; }
+case "$FAIL_ON" in
+  none) exit 0 ;;
+  hole) [ "$(count hole)" -eq 0 ] ;;
+  axiom) [ "$(( $(count hole) + $(count axiom) ))" -eq 0 ] ;;
+  any) [ "$(count any)" -eq 0 ] ;;
+esac
diff --git a/scripts/census/render-catalogue.sh b/scripts/census/render-catalogue.sh
new file mode 100644
index 00000000..e14f7d3d
--- /dev/null
+++ b/scripts/census/render-catalogue.sh
@@ -0,0 +1,55 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Render the catalogue (AsciiDoc) from the committed census rows.
+#
+# Usage: render-catalogue.sh CENSUS_DIR > catalogue.adoc
+#   CENSUS_DIR holds catalogue-rows.jsonl (build-rows.sh), repos.jsonl and
+#   unreachable.jsonl. Output depends on those files only, so
+#   `just catalogue-check` can prove the committed catalogue is current.
+set -euo pipefail
+C=$1
+
+table() { # $1 = class
+  echo '[cols="3,1,1,4,1,1,1,1,1,3",options="header"]'
+  echo '|==='
+  echo '|Repository |Own files |Fixtures |Provers (files) |Declarations |Holes |Axioms |Unsafe |Policy |Proof-status doc'
+  jq -sr --arg c "$1" '
+    map(select(.class == $c))
+    | sort_by(-.own_files, .repo)[]
+    | "\n|https://github.com/\(.repo)[\(.repo)] |\(.own_files) |\(.fixture_files) |\(.provers) |\(.declarations) |\(.holes) |\(.axioms) |\(.unsafe) |\(.policy) |\(if .status_doc == "" then "—" else "`" + .status_doc + "`" end)"
+  ' "$C/catalogue-rows.jsonl"
+  echo '|==='
+}
+
+cat <<EOF
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Estate maths catalogue
+:toc:
+
+Generated by \`scripts/census/render-catalogue.sh\` from the census of
+$(jq -s length "$C/repos.jsonl") repositories. Do not edit by hand; rerun the census.
+
+Each row is a repository with proof files of its own, after the files the RSR
+template ships as boilerplate are set aside. *Theory* and *engineering* are a
+first-pass sort (more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK files
+reads as theory); confirm each row against PROOF-POLICY before relying on it.
+Declarations are top-level names found by keyword and signature rules, so
+Agda and Idris2 counts include helpers. Hole, axiom, unsafe and policy counts
+come from proof-craft's \`proof-holes.sh\`: textual candidates, not kernel
+verdicts.
+
+== Theory
+
+$(table theory)
+
+== Engineering (APIs, ABIs, code)
+
+$(table engineering)
+
+== Not reached
+
+These repositories could not be cloned (private, no credentials in the census
+session):
+
+$(jq -r '"* " + .repo' "$C/unreachable.jsonl")
+EOF
diff --git a/scripts/census/run-census.sh b/scripts/census/run-census.sh
new file mode 100644
index 00000000..18fba13c
--- /dev/null
+++ b/scripts/census/run-census.sh
@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Re-run the whole census and regenerate the catalogue.
+#
+# Usage: run-census.sh [REPO_LIST]
+#   REPO_LIST: one OWNER/REPO per line. Default: every non-fork repo in
+#   docs/catalogue/census/repos.jsonl. Refresh that file first when repos are
+#   added; the GitHub listing is not scriptable from agent sessions, so it is
+#   an input.
+#
+# Raw, path-level output (clones, per-file rows, summary.md) goes to
+# MATHESIS_WORK (default: a fresh temporary directory) and is not committed.
+# Only the per-repo rows and the rendered catalogue are written into the repo.
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+census=$here/../../docs/catalogue/census
+work=${MATHESIS_WORK:-$(mktemp -d)}
+mkdir -p "$work"
+cp "$census/repos.jsonl" "$work/repos.jsonl"
+if [ -n "${1:-}" ]; then
+  cp "$1" "$work/census-list.txt"
+else
+  jq -r 'select(.fork|not) | .full_name | select(test("/awesome-")|not)' "$census/repos.jsonl" > "$work/census-list.txt"
+fi
+list=$work/census-list.txt
+rm -rf "$work/out"
+while IFS= read -r repo; do
+  [ -n "$repo" ] && MATHESIS_DATA=$work bash "$here/census-repo.sh" "$repo" || true
+done < "$list"
+MATHESIS_DATA=$work bash "$here/summarise.sh"
+cp "$work/unreachable.jsonl" "$census/unreachable.jsonl"
+bash "$here/build-rows.sh" "$work" "$census/template-paths.txt" > "$census/catalogue-rows.jsonl"
+bash "$here/render-catalogue.sh" "$census" > "$here/../../docs/catalogue/catalogue.adoc"
+echo "raw census kept in $work"
diff --git a/scripts/census/summarise.sh b/scripts/census/summarise.sh
new file mode 100644
index 00000000..8483dd17
--- /dev/null
+++ b/scripts/census/summarise.sh
@@ -0,0 +1,104 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+set -uo pipefail
+M=${MATHESIS_DATA:?set MATHESIS_DATA to the census work directory}
+cd "$M" || exit 1
+cat_sorted() { find out -name "*.$1.jsonl" -print0 | sort -z | xargs -0 cat 2>/dev/null | jq -cS . ; }
+cat_sorted files > files.jsonl
+cat_sorted decls > decls.jsonl
+cat_sorted holes > holes.jsonl
+cat_sorted agdaopts > agda-options.jsonl
+cat_sorted status > repos-with-status.jsonl
+cat_sorted unreach > unreachable.jsonl
+
+PROVER='def prover: (.ext) as $e |
+  if ($e|test("^(agda|lagda|lagda.md|agda-lib)$")) then "agda"
+  elif ($e|test("^(idr|lidr|ipkg)$")) then "idris2"
+  elif ($e|test("^(lean|lean-toolchain|.lean-toolchain|lakefile.lean|lakefile.toml)$")) then "lean"
+  elif ($e|test("^(v|_CoqProject)$")) then "rocq"
+  elif $e=="thy" then "isabelle"
+  elif ($e|test("^(tla|cfg)$")) then "tla"
+  elif $e=="dk" then "dedukti" elif $e=="lp" then "lambdapi"
+  elif $e=="smt2" then "smtlib" elif ($e|test("^(tptp|p)$")) then "tptp"
+  elif ($e|test("^(ads|adb|gpr)$")) then "spark" elif $e=="mlw" then "why3"
+  elif $e=="fst" then "fstar" elif $e=="dfy" then "dafny" elif $e=="als" then "alloy" else $e end;'
+CORPUS_RE='(^|/)(tests?|fixtures?|test-fixtures|testdata|test-data|examples?|benchmarks?|benches|bench|corpus|corpora|samples?|external_corpora|third_party|vendor|training_data)(/|$)'
+
+total=$(wc -l < repos.jsonl)
+forks=$(jq -s '[.[]|select(.fork)]|length' repos.jsonl)
+awesome=$(jq -s '[.[]|select((.fork|not) and (.full_name|test("/awesome-")))]|length' repos.jsonl)
+census=$(wc -l < census-list.txt)
+unreach=$(wc -l < unreachable.jsonl)
+witha=$(jq -rs '[.[].repo]|unique|length' files.jsonl)
+nfiles=$(wc -l < files.jsonl); ndecls=$(wc -l < decls.jsonl)
+
+{
+echo "# Maths census: proof and formal-verification artefacts"
+echo
+echo "Generated $(date -u +%Y-%m-%dT%H:%MZ) from blobless shallow clones of each repo's default branch HEAD."
+echo
+echo "## Totals"
+echo
+echo "| measure | count |"
+echo "|---|---|"
+echo "| repos enumerated (hyperpolymath, metadatastician, catachresis-colloquium, stuff-of-awe) | $total |"
+echo "| forks skipped | $forks |"
+echo "| awesome-* list repos skipped | $awesome |"
+echo "| repos in census | $census |"
+echo "| unreachable (clone failed) | $unreach |"
+echo "| repos with any proof artefact | $witha |"
+echo "| proof artefact files | $nfiles |"
+echo "| declarations extracted | $ndecls |"
+echo "| hole-scanner findings | $(wc -l < holes.jsonl) |"
+echo
+echo "Hole classes (from proof-holes.sh): hole = unfinished proof, axiom = trusted base grows, unsafe = checker switched off, policy = estate rule (Agda without --safe, import Mathlib)."
+echo
+echo "## Repos with artefacts (sorted by declarations)"
+echo
+echo "| repo | provers (files) | decls | holes | axioms | unsafe | policy | Agda --safe / without | proof-status doc |"
+echo "|---|---|---|---|---|---|---|---|---|"
+jq -rn --slurpfile F files.jsonl --slurpfile D decls.jsonl --slurpfile H holes.jsonl --slurpfile A agda-options.jsonl --slurpfile S repos-with-status.jsonl "$PROVER"'
+  ($F|map(.repo)|unique) as $repos
+  | [ $repos[] as $r |
+      { r:$r,
+        p: ([$F[]|select(.repo==$r)|prover]|group_by(.)|map("\(.[0]) \(length)")|join(", ")),
+        d: ([$D[]|select(.repo==$r)]|length),
+        h: ([$H[]|select(.repo==$r and .class=="hole")]|length),
+        a: ([$H[]|select(.repo==$r and .class=="axiom")]|length),
+        u: ([$H[]|select(.repo==$r and .class=="unsafe")]|length),
+        po: ([$H[]|select(.repo==$r and .class=="policy")]|length),
+        as: ([$A[]|select(.repo==$r and has("options") and .safe)]|length),
+        an: ([$A[]|select(.repo==$r and has("options") and (.safe|not))]|length),
+        s: ([$S[]|select(.repo==$r)|.path]|join("<br>")) } ]
+  | sort_by(-.d, .r)[]
+  | "| \(.r) | \(.p) | \(.d) | \(.h) | \(.a) | \(.u) | \(.po) | \(if (.as+.an)>0 then "\(.as) / \(.an)" else "" end) | \(.s) |"'
+echo
+echo "## Possible test corpora rather than obligations"
+echo
+echo "Repos where artefact paths sit under tests/, fixtures/, examples/, benchmarks/, corpus/, vendor/ and similar, plus echidna's proofs/<prover>/ tree (prover test corpus). Flagged, not dropped; the counts above still include them."
+echo
+echo "| repo | files under corpus-like paths / all artefact files | sample prefixes |"
+echo "|---|---|---|"
+jq -rn --slurpfile F files.jsonl --arg re "$CORPUS_RE" '
+  ($F|map(.repo)|unique)[] as $r
+  | [$F[]|select(.repo==$r)] as $fs
+  | [$fs[]|select((.path|test($re)) or ($r=="hyperpolymath/echidna" and (.path|test("^proofs/[^/]+/"))))] as $c
+  | select(($c|length)>0)
+  | ($c|map(.path|split("/")|.[0:2]|join("/"))|group_by(.)|map("\(.[0]) (\(length))")|sort_by(.)|.[0:6]|join("; ")) as $pre
+  | "| \($r) | \($c|length) / \($fs|length) | \($pre) |"'
+echo
+echo "## Proof-status documents"
+echo
+jq -r '"- \(.repo): `\(.path)`"' repos-with-status.jsonl
+echo
+echo "## Unreachable"
+echo
+jq -r '"- \(.repo): \(.error)"' unreachable.jsonl
+echo
+echo "## Method and caveats"
+echo
+echo "- Enumeration used the session's list_repos tool (per-letter substring queries). Every repo it returned has pushed_at on or after 2026-09-15, so repos untouched since then may be missing from the listing."
+echo "- Declarations are grep/awk best effort. Agda and Idris2 count every column-0 \`name : type\` signature (helpers included), plus data/record names and postulated names; Lean/Rocq/Isabelle use keyword rules; TLA+ counts THEOREM/LEMMA and .cfg INVARIANT/PROPERTY names. SMT-LIB, TPTP, Dafny, F*, Why3, Alloy and SPARK files are counted as files only."
+echo "- .v files count only in repos with Rocq signs (_CoqProject, dune with coq, or a .v containing Require/Theorem); Verilog-looking files are skipped. .p counts only with TPTP formulas, .lp only with Lambdapi keywords, .ads/.adb only when the repo has a .gpr or SPARK_Mode."
+echo "- Hole counts are textual (proof-holes.sh); a kernel-level audit is the authority."
+} > summary.md