diff --git a/docs/atlas/census/rows.jsonl b/docs/atlas/census/rows.jsonl
index d7e67fe..0f3ae7f 100644
--- a/docs/atlas/census/rows.jsonl
+++ b/docs/atlas/census/rows.jsonl
@@ -24,10 +24,10 @@
 {"axioms":0,"censused_at":"2026-11-10T21:47:20Z","class":"engineering","commit":"46b4b8b3db767d69658daf62b6bbe45474b1094b","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,"censused_at":"2026-11-10T21:47:22Z","class":"engineering","commit":"065abbeab23e694f9a46f00683a8ece26d04c1ac","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,"censused_at":"2026-11-10T21:47:23Z","class":"theory","commit":"0c868315a7985d1a3409c523a2ff616acb2763c4","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,"censused_at":"2026-11-10T21:47:27Z","class":"theory","commit":"9903e7694418c3017c54806e8558bdf5414b8f37","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
-{"axioms":1,"censused_at":"2026-11-10T21:47:42Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","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,"censused_at":"2026-11-10T21:47:47Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","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,"censused_at":"2026-11-10T21:47:57Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"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,"censused_at":"2026-11-13T18:29:20Z","class":"theory","commit":"93fbfaf1dfa08ac9e48137bc22d99c6909986d68","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":0,"censused_at":"2026-11-13T18:29:28Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","declarations":236,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/ExactCounts.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":0,"censused_at":"2026-11-13T18:29:34Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0}
+{"axioms":1,"censused_at":"2026-11-13T18:29:37Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"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,"censused_at":"2026-11-10T22:40:18Z","class":"theory","commit":"4dbd1adc08e50fb526eb756519634e67c63ac492","declarations":107,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"agda 13","repo":"hyperpolymath/MetaManifold-WebUI","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
 {"axioms":0,"censused_at":"2026-11-10T21:48:16Z","class":"theory","commit":"a92a9e2fd5f0b43d0209ad92f1076aef2bddf520","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,"censused_at":"2026-11-10T21:48:22Z","class":"engineering","commit":"84b6e3644840233c02e660612fccc539cb66ddd2","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/SMTLib.jl","status_doc":"","unsafe":0}
diff --git a/docs/atlas/generated/catalogue.adoc b/docs/atlas/generated/catalogue.adoc
index 37bd8b6..4759ac3 100644
--- a/docs/atlas/generated/catalogue.adoc
+++ b/docs/atlas/generated/catalogue.adoc
@@ -83,9 +83,9 @@ than one.
 
 |https://github.com/hyperpolymath/nextgen-typing[hyperpolymath/nextgen-typing] |16 |11 |agda 3, lean 6, rocq 7 |118 |4 |0 |0 |0 |`PROOF-STATUS.adoc`
 
-|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`
+|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |0 |0 |0 |`proofs/PROOF-STATUS.md`
 
-|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/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |0 |0 |0 |`proofs/PROOF-STATUS.md`
 
 |https://github.com/hyperpolymath/gitbot-fleet[hyperpolymath/gitbot-fleet] |15 |3 |agda 2, lean 4, rocq 3, idris2 6 |82 |5 |0 |0 |0 |`PROOF-NEEDS.adoc`
 
@@ -103,7 +103,7 @@ than one.
 
 |https://github.com/hyperpolymath/CompositionalCounts.jl[hyperpolymath/CompositionalCounts.jl] |10 |0 |agda 10 |184 |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/hyperpolymath/ExactTests.jl[hyperpolymath/ExactTests.jl] |9 |0 |agda 9 |44 |0 |0 |0 |0 |—
 
 |https://github.com/hyperpolymath/boinc-boinc[hyperpolymath/boinc-boinc] |8 |0 |lean 8 |46 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
 
diff --git a/docs/atlas/generated/index.json b/docs/atlas/generated/index.json
index 2dfa188..5e84bd3 100644
--- a/docs/atlas/generated/index.json
+++ b/docs/atlas/generated/index.json
@@ -1 +1 @@
-{"count":249,"records":[{"axioms":0,"censused_at":"2026-11-10T21:45:08Z","class":"engineering","commit":"ba16e54ec9658a75e28fc2a9376d4bc55fd91b70","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,"censused_at":"2026-11-10T21:45:10Z","class":"engineering","commit":"21b166195da6cb083166e1021a1681a92a2f2b49","declarations":73,"fixture_files":0,"holes":0,"own_files":11,"policy":1,"provers":"agda 1, lean 1, rocq 1, idris2 7, tla 1","repo":"catachresis-colloquium/chronicles-of-slavia","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:18Z","class":"engineering","commit":"f1e9d369ec2b796622afaac627f68704c69ed5b7","declarations":19,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"catachresis-colloquium/cytoville","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:28Z","class":"engineering","commit":"450c8a46e0f16ef647c0247439c6042f8a714e9b","declarations":199,"fixture_files":3,"holes":0,"own_files":20,"policy":1,"provers":"agda 1, lean 1, rocq 1, idris2 16, tla 1","repo":"catachresis-colloquium/enaction-engine","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:37Z","class":"engineering","commit":"57d8e78405dcea5d8fe697ee0d8c2cc4c641833f","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:38Z","class":"engineering","commit":"3be90f447b166841f18afe30f4a2188c73beb575","declarations":274,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"catachresis-colloquium/evil-weevil","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:54Z","class":"engineering","commit":"329d8da20534c66fea30023531c665a686150912","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":2,"censused_at":"2026-11-10T21:44:58Z","class":"engineering","commit":"b0c02798635b5096ca9952c4167ddbda148b7def","declarations":131,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 9, creusot 3","repo":"catachresis-colloquium/IDApTIK","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:07Z","class":"theory","commit":"77dddc862f5a95015114a6e736a1097d4d474ac1","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,"censused_at":"2026-11-10T21:46:10Z","class":"engineering","commit":"6d898af53623d9a091e62455f6463fd231594d5f","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:12Z","class":"engineering","commit":"d6e5557e4f7dac69de42ca817f979e564a77dc37","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:20Z","class":"engineering","commit":"ef10ba55860efed7bdb18f8d1110adf2c4873c1e","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,"censused_at":"2026-11-10T21:46:22Z","class":"engineering","commit":"e6ab08b9148523cd53ca4fddd01384dc99c6e88b","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-STATUS.adoc","unsafe":0},{"axioms":8,"censused_at":"2026-11-10T21:46:28Z","class":"engineering","commit":"3fb8b0d46ae216be3bbff80653d2a0b1187698ee","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,"censused_at":"2026-11-10T21:46:33Z","class":"engineering","commit":"b524e87c74b3a0d22e10a12c61161d5861e7680f","declarations":60,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"lean 1, idris2 7","repo":"catachresis-colloquium/sr71-blackglider","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:39Z","class":"engineering","commit":"4f929d44f604539dce235bf49b7ee1b445a6d671","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:40Z","class":"engineering","commit":"e2b5f82e10e50839508b5447a6ff81a1f1b5f850","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:41Z","class":"engineering","commit":"b291b110595527b9395e6597de64be7e3aa13ab3","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,"censused_at":"2026-11-10T21:46:46Z","class":"engineering","commit":"41987f60856bfee08578d603ea1718239bd918e8","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,"censused_at":"2026-11-10T21:46:59Z","class":"engineering","commit":"7897967a049004c8d4f0b72081e8c3ef7ab092f2","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:03Z","class":"engineering","commit":"5aa5d4900c1021e2eec540df22b456099831c893","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":87,"censused_at":"2026-11-10T21:48:28Z","class":"theory","commit":"ad69ddfa6214b0ffa0bbc794ac816b00b650c072","declarations":1074,"fixture_files":0,"holes":7,"own_files":42,"policy":4,"provers":"agda 7, lean 11, rocq 16, isabelle 2, idris2 5, smt-atp 1","repo":"hyperpolymath/absolute-zero","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:48:49Z","class":"engineering","commit":"d4232bb327652bc9cec8f640d36f3894ee7806e2","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":0,"censused_at":"2026-11-10T21:48:52Z","class":"theory","commit":"a4d02e170d68f63efc0652fa84eb6b1fe6e7de4a","declarations":568,"fixture_files":0,"holes":0,"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,"censused_at":"2026-11-10T21:49:15Z","class":"engineering","commit":"c9e65a6b18e1adc2c3d4f27cb1f9b72dca6098e2","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:17Z","class":"engineering","commit":"4bdd96dbed6fc9f77cf7ede31bbb3987af35f744","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/affinescriptiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:23Z","class":"engineering","commit":"75018359dfb855e5637c3aafdf69b1c0fb66b282","declarations":139,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/alloyiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:27Z","class":"engineering","commit":"e6f8b90913f0ab072bdbe59bc1409e1853ec215c","declarations":777,"fixture_files":0,"holes":39,"own_files":64,"policy":0,"provers":"idris2 39, spark 20, other 5","repo":"hyperpolymath/ambientops","status_doc":"PROOF-NEEDS.adoc","unsafe":8},{"axioms":0,"censused_at":"2026-11-10T21:50:07Z","class":"engineering","commit":"20116e5cfcfabed2d8126c452a8e478d89d36ba8","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/anvomidaviser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:50:10Z","class":"engineering","commit":"7ad7d87a04592696cba45482c379f8b8e6b107b4","declarations":107,"fixture_files":1,"holes":0,"own_files":18,"policy":0,"provers":"idris2 18","repo":"hyperpolymath/anytype","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:50:20Z","class":"theory","commit":"e793355de77d378e4aa758d51a685dfb0aa38cef","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,"censused_at":"2026-11-10T21:50:31Z","class":"engineering","commit":"2193fa2d7cc3a266cde1a164f074dcaed9da18f9","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,"censused_at":"2026-11-10T21:52:02Z","class":"engineering","commit":"98433ef9fad9f8e4f77d1899f8a8697ff656fcf5","declarations":128,"fixture_files":0,"holes":0,"own_files":24,"policy":4,"provers":"agda 4, idris2 4, smt-atp 16","repo":"hyperpolymath/atoma","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:16Z","class":"engineering","commit":"54bb38fe62ead30b92ff0266210c770dd264199e","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/atsiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:21Z","class":"theory","commit":"a235db843b950c8a5f8ab67109d60831e1421741","declarations":7,"fixture_files":1,"holes":0,"own_files":4,"policy":0,"provers":"agda 4","repo":"hyperpolymath/autoformal-fidelity","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:13Z","class":"engineering","commit":"3b7f9abc77c72c3b32b531c073e03d507adb4cbe","declarations":145,"fixture_files":0,"holes":3,"own_files":12,"policy":0,"provers":"idris2 11, creusot 1","repo":"hyperpolymath/Axiom.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:37Z","class":"engineering","commit":"8f4b2dc50cf67b158c6443c2d924a18766f141b5","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,"censused_at":"2026-11-10T21:52:39Z","class":"engineering","commit":"f21c9340f47f8d14791623730edcddd0625508a2","declarations":95,"fixture_files":9,"holes":0,"own_files":14,"policy":0,"provers":"lean 3, idris2 11","repo":"hyperpolymath/betlang","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:50Z","class":"engineering","commit":"6b88aed9e8520603bf0b3e2a7ee5265366b81cc6","declarations":173,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/betlangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:56Z","class":"engineering","commit":"eb4c60be3d43812ba8787fc1fe9bcbecc523befc","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 4, other 2","repo":"hyperpolymath/bitfuckit","status_doc":"","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T21:53:13Z","class":"engineering","commit":"fd95f822aee8a7333b670a764397ecffcaa26903","declarations":166,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/bofig","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:53:16Z","class":"theory","commit":"9162a8b1049166934e75b038845beccd2bbf9e9a","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/bofj-kitt","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:53:20Z","class":"theory","commit":"80ab4c09c9d85819e95a69de29a5c0296f052416","declarations":46,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"lean 8","repo":"hyperpolymath/boinc-boinc","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":22,"censused_at":"2026-11-10T21:53:24Z","class":"engineering","commit":"84014d43b903cbda6bab65e592bd345b1842d3be","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":"docs/proof-debt.adoc","unsafe":0},{"axioms":3,"censused_at":"2026-11-10T21:53:35Z","class":"engineering","commit":"cb2180e4be173b1991cd6e6672a5016dc2669809","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,"censused_at":"2026-11-10T21:47:18Z","class":"engineering","commit":"853e2c8ad9254106f43028cd9cd90ee8fe8fc9f9","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,"censused_at":"2026-11-10T21:54:39Z","class":"engineering","commit":"a0974780a449d12593544e8e8cf2ddb107d979ca","declarations":132,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/bqniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:54:52Z","class":"engineering","commit":"cae53d9ef9e7adc7095bf64613bafc6a5e4e86a4","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,"censused_at":"2026-11-10T21:54:55Z","class":"engineering","commit":"07d80c2eca88b39e94be7fec89129f187d6b97e9","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/chapeliser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:54:59Z","class":"engineering","commit":"114ba3aba3eb994a94d724ab906243801c4c4ff1","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,"censused_at":"2026-11-10T21:55:02Z","class":"theory","commit":"96ff750d3c1ba518d59dc1b4f2247de81a2aeb76","declarations":214,"fixture_files":10,"holes":0,"own_files":34,"policy":1,"provers":"agda 34","repo":"hyperpolymath/choreographic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:15Z","class":"engineering","commit":"d04055f4a26c4a0a5fa4f5149d40f0c42aeac274","declarations":6,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"spark 2, creusot 1, other 1","repo":"hyperpolymath/cicd-squabbler","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:30Z","class":"engineering","commit":"f737325ef4a17816adf3066b48242dc0416debde","declarations":46,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/civic-connect","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:20Z","class":"engineering","commit":"46b4b8b3db767d69658daf62b6bbe45474b1094b","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,"censused_at":"2026-11-10T21:47:22Z","class":"engineering","commit":"065abbeab23e694f9a46f00683a8ece26d04c1ac","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,"censused_at":"2026-11-10T21:55:43Z","class":"engineering","commit":"fedbceb85568d65e91b8a97c841af5a925759d12","declarations":0,"fixture_files":1,"holes":0,"own_files":2,"policy":0,"provers":"spark 1, other 1","repo":"hyperpolymath/cloud-sync-tuner","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:46Z","class":"engineering","commit":"65b2be81147fd979e43b9bd931c141abf8de2276","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,"censused_at":"2026-11-10T21:55:48Z","class":"engineering","commit":"e310d0803588e5d3aa475f56adc340145bf81cbc","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,"censused_at":"2026-11-10T21:47:23Z","class":"theory","commit":"0c868315a7985d1a3409c523a2ff616acb2763c4","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,"censused_at":"2026-11-10T21:47:27Z","class":"theory","commit":"9903e7694418c3017c54806e8558bdf5414b8f37","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:50Z","class":"engineering","commit":"8408a700d6f5b4eaae632feb222b2cb60ce8061a","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,"censused_at":"2026-11-10T21:55:55Z","class":"engineering","commit":"77476a20a044cc18d41e1a33742dafbbbe428895","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,"censused_at":"2026-11-10T21:55:58Z","class":"engineering","commit":"1e4289bc472f74d2eb85172dba893bc7afe7ab09","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,"censused_at":"2026-11-10T21:56:00Z","class":"theory","commit":"233905942801b9fc45cc7f51edf2ec9c612cd076","declarations":13,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"lean 1, tla 2","repo":"hyperpolymath/contractiles","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:56:21Z","class":"engineering","commit":"ae01453fbae72983ac8a6ed6b78b02baabcbb2e2","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,"censused_at":"2026-11-10T21:56:36Z","class":"engineering","commit":"25718c706902f44ba8a4f437124405f143e99942","declarations":146,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/dafniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:56:40Z","class":"engineering","commit":"c334dab63a25995ed5ce1256e4e633bad21adacd","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,"censused_at":"2026-11-10T21:56:42Z","class":"engineering","commit":"a1c1df44bbaa86a9f6981f75be303ca37e643a29","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,"censused_at":"2026-11-10T21:56:49Z","class":"engineering","commit":"039cdf27321459eb1343c94a3a217d5c733e801d","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":6,"censused_at":"2026-11-10T21:56:59Z","class":"engineering","commit":"4b6101952339dcb960bc31cf9dbe5bd979d7ed04","declarations":4024,"fixture_files":40,"holes":91,"own_files":649,"policy":2,"provers":"agda 2, lean 3, rocq 274, idris2 347, spark 18, tla 2, other 3","repo":"hyperpolymath/developer-ecosystem","status_doc":"PROOF-NEEDS.adoc","unsafe":61},{"axioms":0,"censused_at":"2026-11-10T22:01:06Z","class":"engineering","commit":"fd65af8133a11883bac8743a83627d72af90160c","declarations":17,"fixture_files":0,"holes":2,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/dictask","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:01:15Z","class":"engineering","commit":"bb040507c7b0a7fd4f9fb97b009d0b06e904be5e","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"hyperpolymath/docmatrix","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:01:21Z","class":"engineering","commit":"cbd8445445512559b49a300bc7f26d4ec05273f4","declarations":223,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/docudactyl","status_doc":"","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:01:29Z","class":"engineering","commit":"1187411746c607ece0e2ecb39e1f8fac1cb87aa6","declarations":1969,"fixture_files":21,"holes":3,"own_files":170,"policy":27,"provers":"agda 28, lean 18, rocq 9, isabelle 6, idris2 48, spark 17, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4","repo":"hyperpolymath/echidna","status_doc":"docs/PROOF-STATUS.adoc","unsafe":4},{"axioms":0,"censused_at":"2026-11-10T22:02:35Z","class":"theory","commit":"207ccc5191657d5e84bd8b526c2552116f7b865f","declarations":82,"fixture_files":0,"holes":5,"own_files":12,"policy":0,"provers":"agda 2, lean 4, rocq 3, idris2 3","repo":"hyperpolymath/echidnabot","status_doc":"docs/PROOF-STATUS.adoc","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:02:39Z","class":"theory","commit":"03067a67b785bd11a1b788527fdd1d2a69fdcaf0","declarations":1759,"fixture_files":0,"holes":0,"own_files":165,"policy":1,"provers":"agda 163, lean 1, rocq 1","repo":"hyperpolymath/echo-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":5,"censused_at":"2026-11-10T22:03:32Z","class":"theory","commit":"48ea0e4a4461b0c1ae5f44e449dcad90762ec378","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,"censused_at":"2026-11-10T22:03:52Z","class":"engineering","commit":"da7e92957b2fbf781f0a69f4534147491c02cc5c","declarations":121,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/eclexiaiser","status_doc":"","unsafe":0},{"axioms":12,"censused_at":"2026-11-10T22:03:58Z","class":"engineering","commit":"59e0343c538db8130cff5780a3bb6b6b4b81538a","declarations":719,"fixture_files":0,"holes":0,"own_files":48,"policy":0,"provers":"rocq 24, idris2 24","repo":"hyperpolymath/ephapax","status_doc":"formal/PROOF-STATUS.a2ml","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:04:21Z","class":"engineering","commit":"f35af47e7c33e29f0f8461b944809abdb6cfa43b","declarations":133,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ephapaxiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:25Z","class":"theory","commit":"bfcee6e235dd8802e301ea92fa0d445b1c94b807","declarations":513,"fixture_files":28,"holes":0,"own_files":60,"policy":0,"provers":"agda 60","repo":"hyperpolymath/epistemic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:48Z","class":"engineering","commit":"bc393f8e9f61df0dae448f046b1544a5218d1a16","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":1,"censused_at":"2026-11-10T21:47:42Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","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,"censused_at":"2026-11-10T21:47:47Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":1,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:57Z","class":"engineering","commit":"c0b8767082b67044d291306d668b8cb2e8510dfa","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,"censused_at":"2026-11-10T22:04:59Z","class":"engineering","commit":"25d5aa7554908fbc7d5d5013fdde761b7675da8c","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,"censused_at":"2026-11-10T22:05:01Z","class":"engineering","commit":"413f8a08c808ecefe10de4496679676da62098f4","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,"censused_at":"2026-11-10T22:05:09Z","class":"engineering","commit":"8cc53f2d4bb204cb75f3bc4a651799328d8c2d0e","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,"censused_at":"2026-11-10T22:05:17Z","class":"theory","commit":"034d50ce2dae302ea4b58789833614a90a360598","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,"censused_at":"2026-11-10T22:05:31Z","class":"engineering","commit":"7d974119e263390ace42b8d2a0f585f6b8e289c0","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/flatracoon","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:36Z","class":"engineering","commit":"7caf52310615f71528c30a48c6829bf0c317b3da","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"hyperpolymath/formatrix-docs","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:52Z","class":"engineering","commit":"64ea085964818dce3fa2c2b5252821baa6287618","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/futharkiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:57Z","class":"engineering","commit":"ffa76ec2c17ac0d01edcbad5e5d3878242471023","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,"censused_at":"2026-11-10T22:06:01Z","class":"theory","commit":"da29c69f1cb82397d2f3e776a853945de6b067dd","declarations":82,"fixture_files":3,"holes":5,"own_files":15,"policy":0,"provers":"agda 2, lean 4, rocq 3, idris2 6","repo":"hyperpolymath/gitbot-fleet","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:15Z","class":"engineering","commit":"50732be0eeaac30bc163b0f2937c1c5afeff38f8","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/glyphbase","status_doc":"","unsafe":0},{"axioms":7,"censused_at":"2026-11-10T22:06:17Z","class":"theory","commit":"bbed3a0c5e314f1a4be28342440dd3aa7323025d","declarations":737,"fixture_files":8,"holes":4,"own_files":53,"policy":0,"provers":"lean 49, idris2 4","repo":"hyperpolymath/gnpl","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:39Z","class":"engineering","commit":"7083d1934dd945482883e66fae47733afbb95409","declarations":10,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/haec","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:45Z","class":"engineering","commit":"da63c6702f9f1d8ca4473dd7e7eb0e25c54f2d5a","declarations":161,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/halideiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:49Z","class":"engineering","commit":"2aa57e653b397f496ddc87258fe81a2710f90b83","declarations":9,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/hermeneia","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:55Z","class":"engineering","commit":"79e784f958e3c57f4cb3f2c6dd3504b3780a27bb","declarations":16,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/heron-polyfeed-reader","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:07:11Z","class":"engineering","commit":"73be9e7eb9c53eaa5207ef70fc75aeef6d3093b1","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,"censused_at":"2026-11-10T22:07:13Z","class":"engineering","commit":"3c00497ee51703c826a85b7aa06fe16547e02d4c","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,"censused_at":"2026-11-10T22:07:14Z","class":"engineering","commit":"c5bb4ffedcd46c85fc04f5511b4fa31122117926","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,"censused_at":"2026-11-10T22:07:16Z","class":"engineering","commit":"14b32c1c302593fe475205e0a90f55a4a97da7b3","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,"censused_at":"2026-11-10T22:07:17Z","class":"engineering","commit":"0f5d47be83fe818ef714d4e6109dbd8069df3d29","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,"censused_at":"2026-11-10T22:07:19Z","class":"engineering","commit":"871dbf1a77cbe6f6fd3eb7b703e98649a710b0d4","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,"censused_at":"2026-11-10T22:07:26Z","class":"engineering","commit":"2ee6ae098f52bd1e0ea97d7d394fa441c25494e2","declarations":680,"fixture_files":24,"holes":3,"own_files":58,"policy":1,"provers":"agda 2, lean 1, rocq 1, idris2 52, tla 2","repo":"hyperpolymath/hypatia","status_doc":"verification/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:07:54Z","class":"engineering","commit":"439f5211635b0f1cceed7058f72a6554da53ad05","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/i-human","status_doc":"","unsafe":0},{"axioms":7,"censused_at":"2026-11-10T22:07:56Z","class":"engineering","commit":"00141a874aefbafa7f175027349cd377623065f0","declarations":77,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/ideas-to-alphas","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:03Z","class":"engineering","commit":"bb9320f7d84e517e23b1fc13ef3ecbe261bfdac0","declarations":122,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/idrisiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:11Z","class":"engineering","commit":"dae1632db8389dad129a1efedb7eb4afad5a76ef","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,"censused_at":"2026-11-10T22:08:15Z","class":"theory","commit":"3a0a8fce3ee95af7e6cc6e6893c0725bf2a25aaf","declarations":16,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/invariant-path","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:17Z","class":"engineering","commit":"843255953c97cf5401118b84344cffb0751e6de3","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,"censused_at":"2026-11-10T22:08:24Z","class":"engineering","commit":"176fa8952e770f1b44a92a2bf98418d65f6ede96","declarations":254,"fixture_files":0,"holes":0,"own_files":18,"policy":0,"provers":"idris2 18","repo":"hyperpolymath/iseriser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:36Z","class":"theory","commit":"12681e2f85226475c7e0e4e79013e7b361eb205a","declarations":223,"fixture_files":12,"holes":0,"own_files":23,"policy":0,"provers":"agda 11, lean 2, rocq 2, idris2 8","repo":"hyperpolymath/januskey","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:51Z","class":"theory","commit":"499038a160a86b9528ccc9c3946ef48659ed9d48","declarations":301,"fixture_files":0,"holes":0,"own_files":16,"policy":0,"provers":"agda 5, lean 10, idris2 1","repo":"hyperpolymath/jtv-lang","status_doc":"verification/PROOF-STATUS.adoc","unsafe":0},{"axioms":9,"censused_at":"2026-11-10T22:08:59Z","class":"engineering","commit":"d5aa02993c04cf7428a1ed60baa91e0c0f673275","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,"censused_at":"2026-11-10T22:09:06Z","class":"engineering","commit":"be909895e9355d6137b1911802b746b8220d50d6","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,"censused_at":"2026-11-10T22:09:08Z","class":"engineering","commit":"19899b48f6cf322d0b5c0667f2c41b22467fae23","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/julianiser","status_doc":"","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T21:47:57Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"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,"censused_at":"2026-11-10T22:09:11Z","class":"engineering","commit":"20f6be5b5a14a48680b236955b5c4ad9033d00d4","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,"censused_at":"2026-11-10T22:09:15Z","class":"engineering","commit":"ef018acb4381f7cbf81a98c5c1dbc05d299fe985","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,"censused_at":"2026-11-10T22:09:17Z","class":"engineering","commit":"948d020226b3110b6792facf856b88c2bc4d8788","declarations":105,"fixture_files":0,"holes":1,"own_files":13,"policy":0,"provers":"idris2 13","repo":"hyperpolymath/kategoria","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":4,"censused_at":"2026-11-10T22:09:24Z","class":"engineering","commit":"ff7ddde1c9fc9161ee031afad6e802aa24940247","declarations":111,"fixture_files":0,"holes":0,"own_files":11,"policy":1,"provers":"agda 5, idris2 6","repo":"hyperpolymath/kitchenspeak","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:09:32Z","class":"engineering","commit":"6f085752c790bbba91e5fa0110a304ea316daa8c","declarations":61,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"agda 2, idris2 3","repo":"hyperpolymath/krl","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:09:36Z","class":"engineering","commit":"7fc73e85e213d94539d3ea00adcd18ccd908180f","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,"censused_at":"2026-11-10T22:09:37Z","class":"engineering","commit":"8207b18d2a36fe19400540481b3b4cdb766c2321","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,"censused_at":"2026-11-10T22:09:40Z","class":"engineering","commit":"b64e5cdda1680432793ee167759fd2aa7bcdeb65","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,"censused_at":"2026-11-10T22:09:50Z","class":"theory","commit":"ca03e7c2b7c93be3057ed308c6c129e056a9edf0","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-STATUS.adoc","unsafe":0},{"axioms":2,"censused_at":"2026-11-10T22:10:08Z","class":"engineering","commit":"b873cefb7161df945535a0a20e19b312cb7f53da","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,"censused_at":"2026-11-10T22:10:18Z","class":"engineering","commit":"392f77ff03b92849940e31b0d965e977bcd0605d","declarations":141,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/lustreiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:10:22Z","class":"engineering","commit":"314750d03ec580e2404c70173ac0a0f6f5ea86be","declarations":11,"fixture_files":1,"holes":0,"own_files":8,"policy":2,"provers":"agda 3, spark 3, other 2","repo":"hyperpolymath/maa-framework","status_doc":"docs/proof-debt.adoc","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:10:27Z","class":"theory","commit":"e479ebc2319438a5db6b8b3f3d8f1a4749014747","declarations":198,"fixture_files":0,"holes":0,"own_files":17,"policy":0,"provers":"lean 17","repo":"hyperpolymath/marches","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:10:34Z","class":"theory","commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","declarations":51,"fixture_files":0,"holes":0,"own_files":6,"policy":1,"provers":"agda 2, lean 3, rocq 1","repo":"hyperpolymath/mathesis","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:40:18Z","class":"theory","commit":"4dbd1adc08e50fb526eb756519634e67c63ac492","declarations":107,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"agda 13","repo":"hyperpolymath/MetaManifold-WebUI","status_doc":"proofs/PROOF-STATUS.md","unsafe":0},{"axioms":26,"censused_at":"2026-11-10T22:10:57Z","class":"theory","commit":"0ba3b9fb0397c2142ea3883330508caa871259e1","declarations":617,"fixture_files":0,"holes":0,"own_files":25,"policy":0,"provers":"rocq 16, idris2 9","repo":"hyperpolymath/my-lang","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:24Z","class":"engineering","commit":"8a6663416f95c20eeeb4fb6401572b18132e1400","declarations":135,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/mylangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:34Z","class":"engineering","commit":"65e6a3029dfb53be3d731df18f256d566fa90fef","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,"censused_at":"2026-11-10T22:11:35Z","class":"engineering","commit":"c5a0bc5466dc724142003779548024d2acf8a941","declarations":0,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"spark 3, other 1","repo":"hyperpolymath/network-ambulance","status_doc":"","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:11:40Z","class":"theory","commit":"49cf1bce1d571f6683e3631f950a1bbb170b78fe","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,"censused_at":"2026-11-10T22:11:47Z","class":"engineering","commit":"4cf7548cd4ce243ab1688710e2540431e74b9442","declarations":279,"fixture_files":3,"holes":0,"own_files":24,"policy":0,"provers":"idris2 24","repo":"hyperpolymath/nextgen-databases","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:55Z","class":"engineering","commit":"21cd89b9f1db1cf3cd1977418eba65a96077eb09","declarations":15,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/nextgen-language-evangeliser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:57Z","class":"theory","commit":"bc91959b41b54043deb2e5776d322bb822990ccc","declarations":118,"fixture_files":11,"holes":4,"own_files":16,"policy":0,"provers":"agda 3, lean 6, rocq 7","repo":"hyperpolymath/nextgen-typing","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:03Z","class":"engineering","commit":"658f28e28fead22987e4c440db787c584678e296","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/nimiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:08Z","class":"engineering","commit":"6739b86bae506a7653155ea22e08f200874bb5cd","declarations":156,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/oblibeniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:12Z","class":"engineering","commit":"c76df124ddb47f18b02377acadae339c0386aea8","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,"censused_at":"2026-11-10T22:12:16Z","class":"theory","commit":"1ba67f7768b7e6020df050fdbf5bee7920b68630","declarations":90,"fixture_files":2,"holes":0,"own_files":20,"policy":0,"provers":"agda 8, lean 6, idris2 6","repo":"hyperpolymath/occupancy-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:30Z","class":"engineering","commit":"aab2fa3bde65a413dcbb8a75064fd063a9bed2c0","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,"censused_at":"2026-11-10T22:12:51Z","class":"engineering","commit":"62f1b8554611e13a87447e6d401c89e997bbe292","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,"censused_at":"2026-11-10T22:12:56Z","class":"engineering","commit":"739d7cbc339ccee76e694520f5a201a3acb142c5","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":2,"censused_at":"2026-11-10T22:13:08Z","class":"theory","commit":"f27d2921c2a577b43306d82fc6a2b42dc0b19447","declarations":625,"fixture_files":0,"holes":0,"own_files":78,"policy":1,"provers":"agda 78","repo":"hyperpolymath/ordinal-notation","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:36Z","class":"engineering","commit":"fa39db2edf79eba611169d91671d9751c3e1d1ec","declarations":157,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/otpiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:40Z","class":"theory","commit":"21be6420f4aa4c2486488b5c8e4031be42384d76","declarations":43,"fixture_files":4,"holes":0,"own_files":7,"policy":0,"provers":"agda 5, lean 1, rocq 1","repo":"hyperpolymath/palimpsest-license","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:45Z","class":"engineering","commit":"15868fee549383c063a4efcf8eaaa75616189943","declarations":65,"fixture_files":1,"holes":0,"own_files":14,"policy":0,"provers":"idris2 5, tla 9","repo":"hyperpolymath/panic-attack","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:51Z","class":"engineering","commit":"d142b63856559e30c134e6d70e4779b9132dd6ae","declarations":169,"fixture_files":11,"holes":0,"own_files":21,"policy":0,"provers":"idris2 17, tla 4","repo":"hyperpolymath/panll","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:59Z","class":"engineering","commit":"2e40cac9e7df54654edcfae9d92a723427d35175","declarations":14,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/panoply","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:03Z","class":"engineering","commit":"c12e76f862c4ea5e85e7c3a283b1372cf0dc37c7","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,"censused_at":"2026-11-10T22:14:10Z","class":"engineering","commit":"c659474f807f0f187c33a99f782a91b03ecac16b","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,"censused_at":"2026-11-10T22:14:12Z","class":"engineering","commit":"a62fd06ab828dce790704e98885cf8e55dc2577c","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,"censused_at":"2026-11-10T22:14:14Z","class":"theory","commit":"b06a951820feb0b99731d85627057915873edeae","declarations":140,"fixture_files":0,"holes":0,"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,"censused_at":"2026-11-10T22:14:20Z","class":"engineering","commit":"6b2b2f6b06a5741c9400162e86978292ec07c9a7","declarations":155,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/phronesiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:23Z","class":"engineering","commit":"b5193824d5638e0dbcd9489a8aa619928e2c9dad","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,"censused_at":"2026-11-10T22:14:29Z","class":"engineering","commit":"5d05ebf85af03ced28c44fb778029923acf3813f","declarations":44,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 2, spark 4, other 1","repo":"hyperpolymath/poly-ssg","status_doc":"","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:14:32Z","class":"engineering","commit":"31f57c30ae577f96540b3c00d49e9b90b4cd3761","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,"censused_at":"2026-11-10T22:14:34Z","class":"engineering","commit":"db0907c0d0b3fd437a58648573bb4fdf9e43178d","declarations":0,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"spark 4, other 1","repo":"hyperpolymath/polyglot-i18n","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:45Z","class":"engineering","commit":"9f0926715bb5d3b42f0290a46c163cfd1f07615a","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ponyiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:49Z","class":"engineering","commit":"52326c5039e9fbeacb7491ab23fde40fc32c38d5","declarations":76,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/presswerk","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:57Z","class":"theory","commit":"75575b27a51b634f8d0ab3845f0fd94930e6177b","declarations":31,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"hyperpolymath/proof-burrower","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":2,"censused_at":"2026-11-10T22:15:04Z","class":"theory","commit":"3d50aa044666c5a0c6ea722231e2bb55e69740a1","declarations":365,"fixture_files":0,"holes":0,"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":368,"censused_at":"2026-11-10T22:15:30Z","class":"engineering","commit":"a7503b2d96c4e292d8a3239304e187a5c31bc4e6","declarations":11166,"fixture_files":60,"holes":22,"own_files":927,"policy":0,"provers":"lean 14, idris2 906, spark 2, tla 1, other 4","repo":"hyperpolymath/proven","status_doc":"docs/proof-debt-triage-tier-a.adoc","unsafe":10},{"axioms":0,"censused_at":"2026-11-10T22:20:40Z","class":"engineering","commit":"24b244ac9c8e51341139cf5e69c27a19bd154645","declarations":47,"fixture_files":1,"holes":0,"own_files":7,"policy":0,"provers":"idris2 6, creusot 1","repo":"hyperpolymath/proven-cicd-and-workflows","status_doc":"","unsafe":0},{"axioms":3,"censused_at":"2026-11-10T22:20:43Z","class":"engineering","commit":"ebc440f3a865565faf95c911a4df04351213dab5","declarations":6242,"fixture_files":0,"holes":3,"own_files":899,"policy":0,"provers":"idris2 899","repo":"hyperpolymath/proven-servers","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:11Z","class":"engineering","commit":"f90bacbe3a5fa1869239fcb9175757509464aa13","declarations":891,"fixture_files":29,"holes":0,"own_files":75,"policy":0,"provers":"idris2 75","repo":"hyperpolymath/proven-tests-and-benches","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:37Z","class":"engineering","commit":"bc45e1a0d34fad39b2717819c5a52da688bb5aae","declarations":12,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/puggle","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:43Z","class":"engineering","commit":"68c1485f0e33dfddc0478618c69bf87454307c87","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,"censused_at":"2026-11-10T22:26:46Z","class":"engineering","commit":"68b7a4ccd035833e68b34f562c3fd965a2f389f6","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:56Z","class":"engineering","commit":"5ebbdc2fcad9e21e42f1b5f1c42a98e3345511f7","declarations":59,"fixture_files":0,"holes":0,"own_files":17,"policy":0,"provers":"idris2 3, spark 13, other 1","repo":"hyperpolymath/raze-tui","status_doc":"","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:27:04Z","class":"engineering","commit":"7464e6ba60e63901ec04e76e069007d925789595","declarations":25,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/recon-silly-ation","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:27:19Z","class":"engineering","commit":"a04b755e70761a0b55a77cf03903bcd642a15258","declarations":7,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 1, spark 2, other 2","repo":"hyperpolymath/reposystem","status_doc":"PROOF-NEEDS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:27:39Z","class":"theory","commit":"6f94640d370f3470bfbc59f76fa233ee5e9f92b0","declarations":391,"fixture_files":23,"holes":0,"own_files":37,"policy":0,"provers":"agda 37","repo":"hyperpolymath/residual-evidence-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:48:16Z","class":"theory","commit":"a92a9e2fd5f0b43d0209ad92f1076aef2bddf520","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,"censused_at":"2026-11-10T22:27:51Z","class":"theory","commit":"a19a5b8d0ad742aa49c9d19e4312c481972d95c1","declarations":467,"fixture_files":12,"holes":0,"own_files":25,"policy":0,"provers":"agda 22, lean 2, rocq 1","repo":"hyperpolymath/resource-algebra","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:28:10Z","class":"engineering","commit":"d94110acfec2b6b0cfc8566594d9bf0a89da33d0","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,"censused_at":"2026-11-10T22:28:16Z","class":"engineering","commit":"3341a1de656eb1657cddcc5c081933fb10549148","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,"censused_at":"2026-11-10T22:28:50Z","class":"engineering","commit":"0dfde85e6745d1f56a22cf49e11a74abb97b4dd5","declarations":136,"fixture_files":0,"holes":0,"own_files":18,"policy":1,"provers":"agda 1, lean 2, rocq 1, idris2 11, tla 3","repo":"hyperpolymath/rsr-template-repo","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:08Z","class":"theory","commit":"c9c4b3995941aa27d51bc5e68ecb67fdafc673fc","declarations":304,"fixture_files":6,"holes":0,"own_files":30,"policy":0,"provers":"agda 22, lean 7, rocq 1","repo":"hyperpolymath/secret-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:23Z","class":"engineering","commit":"ccdba3cca5f928c7e94f13b551c684a5b3a64dd9","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,"censused_at":"2026-11-10T21:48:22Z","class":"engineering","commit":"84b6e3644840233c02e660612fccc539cb66ddd2","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/SMTLib.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:30Z","class":"engineering","commit":"76a661998aea8d9e198ddf368e618fe9ac7d0c01","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,"censused_at":"2026-11-10T22:29:33Z","class":"engineering","commit":"720eb82168adb0947ab624a7e27972c7c7c9f9d6","declarations":223,"fixture_files":0,"holes":0,"own_files":13,"policy":1,"provers":"agda 3, lean 1, rocq 1, idris2 7, tla 1","repo":"hyperpolymath/snifs","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:47Z","class":"engineering","commit":"4abaef5c2607787d6b01b0c06e6e940c60d9bb6c","declarations":0,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"spark 6, other 1","repo":"hyperpolymath/somethings-fishy","status_doc":"PROOF-STATUS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:29:58Z","class":"engineering","commit":"e5b7e7fd9af511a1c339cfbd2824e0cccd03fada","declarations":108,"fixture_files":0,"holes":3,"own_files":18,"policy":0,"provers":"lean 1, idris2 6, spark 8, other 3","repo":"hyperpolymath/ssg-collection","status_doc":"PROOF-NEEDS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:30:05Z","class":"engineering","commit":"077cc55ad239c824ca65923b0924105ab0d94c60","declarations":56,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 4, tla 2","repo":"hyperpolymath/stateful-artefacts","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:30:10Z","class":"theory","commit":"f2de559f2be33c4a81e2550aa6b75ac1689c7bf8","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,"censused_at":"2026-11-10T22:30:13Z","class":"theory","commit":"126a3b86636de66be3c5811ff3a278c61f887b8e","declarations":773,"fixture_files":0,"holes":0,"own_files":102,"policy":0,"provers":"agda 80, lean 22","repo":"hyperpolymath/system-et","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:30:44Z","class":"theory","commit":"6f070d6eb3faaac75acc6fb2f667e81d43effef2","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,"censused_at":"2026-11-10T22:30:50Z","class":"engineering","commit":"a33a1e79864f6c2725cb8e03dd9134df8c5d2c1a","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,"censused_at":"2026-11-10T22:30:53Z","class":"engineering","commit":"e188f42aab2e24758e487516e3e9c107c8947262","declarations":181,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/tlaiser","status_doc":"","unsafe":0},{"axioms":23,"censused_at":"2026-11-10T22:31:04Z","class":"engineering","commit":"a5163f5145c1ff0add007c35cb15aba6b64a7c93","declarations":165,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"agda 2, idris2 5, spark 1, other 1","repo":"hyperpolymath/trigger","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:23Z","class":"theory","commit":"24d1985fd16e5af9baaa854f1496a7067b278a05","declarations":514,"fixture_files":0,"holes":0,"own_files":38,"policy":1,"provers":"agda 10, lean 12, idris2 16","repo":"hyperpolymath/trope-checker","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:38Z","class":"theory","commit":"f2e465c966d14d4986dfc492875cc54653d9751e","declarations":564,"fixture_files":0,"holes":4,"own_files":29,"policy":0,"provers":"lean 20, isabelle 9","repo":"hyperpolymath/tropical-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:48Z","class":"engineering","commit":"a86bba4100d3f27919a154cdefeee60ef64cb5a8","declarations":896,"fixture_files":17,"holes":0,"own_files":52,"policy":0,"provers":"idris2 52","repo":"hyperpolymath/typed-wasm","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:32:05Z","class":"engineering","commit":"aa42bb15d9a2e9363f63dba2815c7d733c13da41","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,"censused_at":"2026-11-10T22:32:11Z","class":"engineering","commit":"5a6592aecca77e90b7d9aced9496ab8eddb5c81f","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,"censused_at":"2026-11-10T22:32:20Z","class":"engineering","commit":"549e08fb25146128f84beebbfbc873456f064a19","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,"censused_at":"2026-11-10T22:32:23Z","class":"engineering","commit":"ba91e87607724066029855dba43b326c2e095a43","declarations":28,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/unified-api-adapter","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:32:29Z","class":"engineering","commit":"56ad8091601b19a211967812b8a7209c32d0020d","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,"censused_at":"2026-11-10T22:32:31Z","class":"engineering","commit":"b8b6f99290e16a1ed0a55c73b8ceabaa3223fb25","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,"censused_at":"2026-11-10T22:32:35Z","class":"engineering","commit":"fc3b6da2446a4755745a33acfe34c6a37a2b00ae","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,"censused_at":"2026-11-10T22:32:38Z","class":"engineering","commit":"dd4e6c87c08402e430f6d7f19c9c58d35db31ed6","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":0,"censused_at":"2026-11-10T22:32:39Z","class":"theory","commit":"48a88eaa58b0c8121fb15a575f263b5a432fad1a","declarations":1031,"fixture_files":0,"holes":5,"own_files":68,"policy":0,"provers":"agda 12, lean 17, rocq 12, isabelle 9, idris2 12, dedukti 1, smt-atp 5","repo":"hyperpolymath/valence-shell","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:04Z","class":"engineering","commit":"5b10cb01ef1b1b5e1b6568a53c2d63c1fa959a81","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,"censused_at":"2026-11-10T22:33:24Z","class":"engineering","commit":"c67b2c33d4a29d96cda30db79af641e99ce175fc","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,"censused_at":"2026-11-10T22:33:30Z","class":"engineering","commit":"703961842e614a7a6760e087cb3dbf5fc855c1c0","declarations":424,"fixture_files":0,"holes":3,"own_files":21,"policy":0,"provers":"rocq 10, idris2 11","repo":"hyperpolymath/verisimdb","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:44Z","class":"engineering","commit":"9633e0113fa3e831c51684965195aa2bf84b9766","declarations":208,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/verisimiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:51Z","class":"engineering","commit":"9d1002f60fda57293cfa00cd85869aae60a8071a","declarations":104,"fixture_files":0,"holes":3,"own_files":10,"policy":0,"provers":"idris2 10","repo":"hyperpolymath/vexometer","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:11Z","class":"engineering","commit":"7fb6c9fa37086b597df380e20a13aa99dbe898af","declarations":58,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/volumod","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:12Z","class":"engineering","commit":"acf709911e868c6308c4b51647c8b4f4f23c42da","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,"censused_at":"2026-11-10T22:34:14Z","class":"theory","commit":"1624f4187f62eed7df026795fce628bfff2689bf","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,"censused_at":"2026-11-10T22:34:22Z","class":"engineering","commit":"8db48b2e4aba9756bd92ce3c81cfdea692a1f504","declarations":143,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/wokelangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:36Z","class":"theory","commit":"2b5ddcc0003f44329222ff88072b0241d368ff02","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,"censused_at":"2026-11-10T22:34:38Z","class":"engineering","commit":"7a37073dfba0cb1ef126113dab8069be52370a12","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,"censused_at":"2026-11-10T22:34:48Z","class":"engineering","commit":"b4d7c252bae52b1698c5a3168a4dc56f57f9fee9","declarations":110,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"agda 1, lean 1, rocq 1, idris2 5","repo":"hyperpolymath/zig-dnssec","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:35:06Z","class":"theory","commit":"a8b4be7fb3273327d81cd84dd3fe9984d336001c","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,"censused_at":"2026-11-10T22:35:35Z","class":"engineering","commit":"aa3ef263ac6ac177a5b0c6fa33e5814c8589101a","declarations":70,"fixture_files":0,"holes":3,"own_files":5,"policy":0,"provers":"idris2 5","repo":"metadatastician/_pathroot","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:35:51Z","class":"engineering","commit":"57b617c7a0a4940f0458f2516e66c69291a0e88a","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,"censused_at":"2026-11-10T22:36:03Z","class":"engineering","commit":"692976054f11764d8daa8736d6e091ed075a2737","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/bowtie-workbench","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:08Z","class":"engineering","commit":"3da26e6c65a1cbcf90ae006e0a2971ce03228641","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,"censused_at":"2026-11-10T22:36:15Z","class":"engineering","commit":"738b209a9370aef3c693801b887709d671827d3b","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/cadastra","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:20Z","class":"engineering","commit":"e8dc1b724a3e47e6a1563a99f715e4252a38f6d5","declarations":91,"fixture_files":0,"holes":18,"own_files":38,"policy":0,"provers":"idris2 8, spark 28, other 2","repo":"metadatastician/cerro-torre","status_doc":"","unsafe":69},{"axioms":0,"censused_at":"2026-11-10T22:36:47Z","class":"engineering","commit":"7a3ba13b808e590c64859e866fae0f6d316cbca8","declarations":38,"fixture_files":3,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"metadatastician/cleave","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:51Z","class":"engineering","commit":"e3d349616ddc48da52b42e606fe36ac1f2f9207a","declarations":27,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"metadatastician/common-signal","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:58Z","class":"engineering","commit":"0e033878078bb11136e7459e2f34cbc0b6c0d6f6","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/first-post","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:37:09Z","class":"engineering","commit":"37a3ad5ac3a19378c84fffc446939954a5d9dd79","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,"censused_at":"2026-11-10T22:37:28Z","class":"engineering","commit":"a8534de4e438e108af0f6f86c802fcef64856d64","declarations":185,"fixture_files":3,"holes":0,"own_files":19,"policy":0,"provers":"idris2 19","repo":"metadatastician/groove","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:37:36Z","class":"theory","commit":"da01ab82aa6b1974276e6f7f064c2beed2f356b4","declarations":640,"fixture_files":7,"holes":0,"own_files":19,"policy":0,"provers":"agda 10, lean 1, rocq 1, idris2 1, tla 6","repo":"metadatastician/hvn-dehallucinator","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:18Z","class":"engineering","commit":"9175fe1971b55e37a9b4c27f3b77b1a40f93b46e","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,"censused_at":"2026-11-10T22:38:26Z","class":"theory","commit":"89ceac3b8685467c664737a98364eef4febb9ff2","declarations":240,"fixture_files":9,"holes":0,"own_files":21,"policy":0,"provers":"agda 13, lean 7, rocq 1","repo":"metadatastician/lintel","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:38Z","class":"engineering","commit":"e5f30dfd891e66c235c6d8c52997a330750c2f1f","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/marid","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:35:13Z","class":"theory","commit":"5cd0c90498384f6f465278a7a3d1a074cd78b45f","declarations":341,"fixture_files":0,"holes":0,"own_files":49,"policy":0,"provers":"agda 13, lean 18, rocq 18","repo":"metadatastician/MetaManifold-Evidence","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:51Z","class":"engineering","commit":"b161660e6b18c9f5b58dceae156fbc4930da92e1","declarations":1149,"fixture_files":8,"holes":4,"own_files":64,"policy":3,"provers":"agda 3, lean 2, rocq 1, idris2 51, tla 7","repo":"metadatastician/paint-type","status_doc":"PROOF-STATUS.adoc","unsafe":8},{"axioms":4,"censused_at":"2026-11-10T22:39:12Z","class":"engineering","commit":"45a86eb761537785ee019315b5ed3148a71b7d17","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,"censused_at":"2026-11-10T22:39:16Z","class":"engineering","commit":"c9f5fce6f18454510ca016608748aa834f1801cd","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,"censused_at":"2026-11-10T22:39:18Z","class":"engineering","commit":"4a6e86cd6417274d9f44c8ac37ceedcd06567446","declarations":23,"fixture_files":0,"holes":4,"own_files":2,"policy":0,"provers":"idris2 2","repo":"metadatastician/selur","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:21Z","class":"engineering","commit":"3804c2071d43213ac935733bda826629fbbe46cf","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:28Z","class":"engineering","commit":"d73229d8220a35f66e99678966797dd6399dda1f","declarations":40,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"metadatastician/standards","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:35Z","class":"engineering","commit":"9858bf0ca5f9bd5c332b24403229da08daa478c9","declarations":294,"fixture_files":8,"holes":0,"own_files":19,"policy":0,"provers":"idris2 18, alloy 1","repo":"metadatastician/stapeln","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:47Z","class":"engineering","commit":"017616c5e31db41c9bd667d2aa35298cab8b81ab","declarations":129,"fixture_files":2,"holes":0,"own_files":26,"policy":0,"provers":"idris2 10, spark 12, creusot 2, verus 1, other 1","repo":"metadatastician/vordr","status_doc":"","unsafe":4},{"axioms":0,"censused_at":"2026-11-10T22:35:29Z","class":"theory","commit":"add77b1edbfd7fc37a25c05e9c08f06af6567756","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"metadatastician/ZenodoDeposits.jl","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0}],"schema":"mathesis.census-atlas/0.1","source":"docs/atlas/census/rows.jsonl","verification":"not_asserted"}
+{"count":249,"records":[{"axioms":0,"censused_at":"2026-11-10T21:45:08Z","class":"engineering","commit":"ba16e54ec9658a75e28fc2a9376d4bc55fd91b70","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,"censused_at":"2026-11-10T21:45:10Z","class":"engineering","commit":"21b166195da6cb083166e1021a1681a92a2f2b49","declarations":73,"fixture_files":0,"holes":0,"own_files":11,"policy":1,"provers":"agda 1, lean 1, rocq 1, idris2 7, tla 1","repo":"catachresis-colloquium/chronicles-of-slavia","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:18Z","class":"engineering","commit":"f1e9d369ec2b796622afaac627f68704c69ed5b7","declarations":19,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"catachresis-colloquium/cytoville","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:28Z","class":"engineering","commit":"450c8a46e0f16ef647c0247439c6042f8a714e9b","declarations":199,"fixture_files":3,"holes":0,"own_files":20,"policy":1,"provers":"agda 1, lean 1, rocq 1, idris2 16, tla 1","repo":"catachresis-colloquium/enaction-engine","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:37Z","class":"engineering","commit":"57d8e78405dcea5d8fe697ee0d8c2cc4c641833f","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:38Z","class":"engineering","commit":"3be90f447b166841f18afe30f4a2188c73beb575","declarations":274,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"catachresis-colloquium/evil-weevil","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:45:54Z","class":"engineering","commit":"329d8da20534c66fea30023531c665a686150912","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":2,"censused_at":"2026-11-10T21:44:58Z","class":"engineering","commit":"b0c02798635b5096ca9952c4167ddbda148b7def","declarations":131,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 9, creusot 3","repo":"catachresis-colloquium/IDApTIK","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:07Z","class":"theory","commit":"77dddc862f5a95015114a6e736a1097d4d474ac1","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,"censused_at":"2026-11-10T21:46:10Z","class":"engineering","commit":"6d898af53623d9a091e62455f6463fd231594d5f","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:12Z","class":"engineering","commit":"d6e5557e4f7dac69de42ca817f979e564a77dc37","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:20Z","class":"engineering","commit":"ef10ba55860efed7bdb18f8d1110adf2c4873c1e","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,"censused_at":"2026-11-10T21:46:22Z","class":"engineering","commit":"e6ab08b9148523cd53ca4fddd01384dc99c6e88b","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-STATUS.adoc","unsafe":0},{"axioms":8,"censused_at":"2026-11-10T21:46:28Z","class":"engineering","commit":"3fb8b0d46ae216be3bbff80653d2a0b1187698ee","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,"censused_at":"2026-11-10T21:46:33Z","class":"engineering","commit":"b524e87c74b3a0d22e10a12c61161d5861e7680f","declarations":60,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"lean 1, idris2 7","repo":"catachresis-colloquium/sr71-blackglider","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:39Z","class":"engineering","commit":"4f929d44f604539dce235bf49b7ee1b445a6d671","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:40Z","class":"engineering","commit":"e2b5f82e10e50839508b5447a6ff81a1f1b5f850","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:46:41Z","class":"engineering","commit":"b291b110595527b9395e6597de64be7e3aa13ab3","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,"censused_at":"2026-11-10T21:46:46Z","class":"engineering","commit":"41987f60856bfee08578d603ea1718239bd918e8","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,"censused_at":"2026-11-10T21:46:59Z","class":"engineering","commit":"7897967a049004c8d4f0b72081e8c3ef7ab092f2","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:03Z","class":"engineering","commit":"5aa5d4900c1021e2eec540df22b456099831c893","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":87,"censused_at":"2026-11-10T21:48:28Z","class":"theory","commit":"ad69ddfa6214b0ffa0bbc794ac816b00b650c072","declarations":1074,"fixture_files":0,"holes":7,"own_files":42,"policy":4,"provers":"agda 7, lean 11, rocq 16, isabelle 2, idris2 5, smt-atp 1","repo":"hyperpolymath/absolute-zero","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:48:49Z","class":"engineering","commit":"d4232bb327652bc9cec8f640d36f3894ee7806e2","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":0,"censused_at":"2026-11-10T21:48:52Z","class":"theory","commit":"a4d02e170d68f63efc0652fa84eb6b1fe6e7de4a","declarations":568,"fixture_files":0,"holes":0,"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,"censused_at":"2026-11-10T21:49:15Z","class":"engineering","commit":"c9e65a6b18e1adc2c3d4f27cb1f9b72dca6098e2","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:17Z","class":"engineering","commit":"4bdd96dbed6fc9f77cf7ede31bbb3987af35f744","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/affinescriptiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:23Z","class":"engineering","commit":"75018359dfb855e5637c3aafdf69b1c0fb66b282","declarations":139,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/alloyiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:49:27Z","class":"engineering","commit":"e6f8b90913f0ab072bdbe59bc1409e1853ec215c","declarations":777,"fixture_files":0,"holes":39,"own_files":64,"policy":0,"provers":"idris2 39, spark 20, other 5","repo":"hyperpolymath/ambientops","status_doc":"PROOF-NEEDS.adoc","unsafe":8},{"axioms":0,"censused_at":"2026-11-10T21:50:07Z","class":"engineering","commit":"20116e5cfcfabed2d8126c452a8e478d89d36ba8","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/anvomidaviser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:50:10Z","class":"engineering","commit":"7ad7d87a04592696cba45482c379f8b8e6b107b4","declarations":107,"fixture_files":1,"holes":0,"own_files":18,"policy":0,"provers":"idris2 18","repo":"hyperpolymath/anytype","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:50:20Z","class":"theory","commit":"e793355de77d378e4aa758d51a685dfb0aa38cef","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,"censused_at":"2026-11-10T21:50:31Z","class":"engineering","commit":"2193fa2d7cc3a266cde1a164f074dcaed9da18f9","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,"censused_at":"2026-11-10T21:52:02Z","class":"engineering","commit":"98433ef9fad9f8e4f77d1899f8a8697ff656fcf5","declarations":128,"fixture_files":0,"holes":0,"own_files":24,"policy":4,"provers":"agda 4, idris2 4, smt-atp 16","repo":"hyperpolymath/atoma","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:16Z","class":"engineering","commit":"54bb38fe62ead30b92ff0266210c770dd264199e","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/atsiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:21Z","class":"theory","commit":"a235db843b950c8a5f8ab67109d60831e1421741","declarations":7,"fixture_files":1,"holes":0,"own_files":4,"policy":0,"provers":"agda 4","repo":"hyperpolymath/autoformal-fidelity","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:13Z","class":"engineering","commit":"3b7f9abc77c72c3b32b531c073e03d507adb4cbe","declarations":145,"fixture_files":0,"holes":3,"own_files":12,"policy":0,"provers":"idris2 11, creusot 1","repo":"hyperpolymath/Axiom.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:37Z","class":"engineering","commit":"8f4b2dc50cf67b158c6443c2d924a18766f141b5","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,"censused_at":"2026-11-10T21:52:39Z","class":"engineering","commit":"f21c9340f47f8d14791623730edcddd0625508a2","declarations":95,"fixture_files":9,"holes":0,"own_files":14,"policy":0,"provers":"lean 3, idris2 11","repo":"hyperpolymath/betlang","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:50Z","class":"engineering","commit":"6b88aed9e8520603bf0b3e2a7ee5265366b81cc6","declarations":173,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/betlangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:52:56Z","class":"engineering","commit":"eb4c60be3d43812ba8787fc1fe9bcbecc523befc","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 4, other 2","repo":"hyperpolymath/bitfuckit","status_doc":"","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T21:53:13Z","class":"engineering","commit":"fd95f822aee8a7333b670a764397ecffcaa26903","declarations":166,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/bofig","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:53:16Z","class":"theory","commit":"9162a8b1049166934e75b038845beccd2bbf9e9a","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/bofj-kitt","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:53:20Z","class":"theory","commit":"80ab4c09c9d85819e95a69de29a5c0296f052416","declarations":46,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"lean 8","repo":"hyperpolymath/boinc-boinc","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":22,"censused_at":"2026-11-10T21:53:24Z","class":"engineering","commit":"84014d43b903cbda6bab65e592bd345b1842d3be","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":"docs/proof-debt.adoc","unsafe":0},{"axioms":3,"censused_at":"2026-11-10T21:53:35Z","class":"engineering","commit":"cb2180e4be173b1991cd6e6672a5016dc2669809","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,"censused_at":"2026-11-10T21:47:18Z","class":"engineering","commit":"853e2c8ad9254106f43028cd9cd90ee8fe8fc9f9","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,"censused_at":"2026-11-10T21:54:39Z","class":"engineering","commit":"a0974780a449d12593544e8e8cf2ddb107d979ca","declarations":132,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/bqniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:54:52Z","class":"engineering","commit":"cae53d9ef9e7adc7095bf64613bafc6a5e4e86a4","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,"censused_at":"2026-11-10T21:54:55Z","class":"engineering","commit":"07d80c2eca88b39e94be7fec89129f187d6b97e9","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/chapeliser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:54:59Z","class":"engineering","commit":"114ba3aba3eb994a94d724ab906243801c4c4ff1","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,"censused_at":"2026-11-10T21:55:02Z","class":"theory","commit":"96ff750d3c1ba518d59dc1b4f2247de81a2aeb76","declarations":214,"fixture_files":10,"holes":0,"own_files":34,"policy":1,"provers":"agda 34","repo":"hyperpolymath/choreographic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:15Z","class":"engineering","commit":"d04055f4a26c4a0a5fa4f5149d40f0c42aeac274","declarations":6,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"spark 2, creusot 1, other 1","repo":"hyperpolymath/cicd-squabbler","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:30Z","class":"engineering","commit":"f737325ef4a17816adf3066b48242dc0416debde","declarations":46,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/civic-connect","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:47:20Z","class":"engineering","commit":"46b4b8b3db767d69658daf62b6bbe45474b1094b","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,"censused_at":"2026-11-10T21:47:22Z","class":"engineering","commit":"065abbeab23e694f9a46f00683a8ece26d04c1ac","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,"censused_at":"2026-11-10T21:55:43Z","class":"engineering","commit":"fedbceb85568d65e91b8a97c841af5a925759d12","declarations":0,"fixture_files":1,"holes":0,"own_files":2,"policy":0,"provers":"spark 1, other 1","repo":"hyperpolymath/cloud-sync-tuner","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:46Z","class":"engineering","commit":"65b2be81147fd979e43b9bd931c141abf8de2276","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,"censused_at":"2026-11-10T21:55:48Z","class":"engineering","commit":"e310d0803588e5d3aa475f56adc340145bf81cbc","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,"censused_at":"2026-11-10T21:47:23Z","class":"theory","commit":"0c868315a7985d1a3409c523a2ff616acb2763c4","declarations":184,"fixture_files":0,"holes":0,"own_files":10,"policy":0,"provers":"agda 10","repo":"hyperpolymath/CompositionalCounts.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-13T18:29:20Z","class":"theory","commit":"93fbfaf1dfa08ac9e48137bc22d99c6909986d68","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:55:50Z","class":"engineering","commit":"8408a700d6f5b4eaae632feb222b2cb60ce8061a","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,"censused_at":"2026-11-10T21:55:55Z","class":"engineering","commit":"77476a20a044cc18d41e1a33742dafbbbe428895","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,"censused_at":"2026-11-10T21:55:58Z","class":"engineering","commit":"1e4289bc472f74d2eb85172dba893bc7afe7ab09","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,"censused_at":"2026-11-10T21:56:00Z","class":"theory","commit":"233905942801b9fc45cc7f51edf2ec9c612cd076","declarations":13,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"lean 1, tla 2","repo":"hyperpolymath/contractiles","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:56:21Z","class":"engineering","commit":"ae01453fbae72983ac8a6ed6b78b02baabcbb2e2","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,"censused_at":"2026-11-10T21:56:36Z","class":"engineering","commit":"25718c706902f44ba8a4f437124405f143e99942","declarations":146,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/dafniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:56:40Z","class":"engineering","commit":"c334dab63a25995ed5ce1256e4e633bad21adacd","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,"censused_at":"2026-11-10T21:56:42Z","class":"engineering","commit":"a1c1df44bbaa86a9f6981f75be303ca37e643a29","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,"censused_at":"2026-11-10T21:56:49Z","class":"engineering","commit":"039cdf27321459eb1343c94a3a217d5c733e801d","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":6,"censused_at":"2026-11-10T21:56:59Z","class":"engineering","commit":"4b6101952339dcb960bc31cf9dbe5bd979d7ed04","declarations":4024,"fixture_files":40,"holes":91,"own_files":649,"policy":2,"provers":"agda 2, lean 3, rocq 274, idris2 347, spark 18, tla 2, other 3","repo":"hyperpolymath/developer-ecosystem","status_doc":"PROOF-NEEDS.adoc","unsafe":61},{"axioms":0,"censused_at":"2026-11-10T22:01:06Z","class":"engineering","commit":"fd65af8133a11883bac8743a83627d72af90160c","declarations":17,"fixture_files":0,"holes":2,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/dictask","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:01:15Z","class":"engineering","commit":"bb040507c7b0a7fd4f9fb97b009d0b06e904be5e","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"hyperpolymath/docmatrix","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:01:21Z","class":"engineering","commit":"cbd8445445512559b49a300bc7f26d4ec05273f4","declarations":223,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 7","repo":"hyperpolymath/docudactyl","status_doc":"","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:01:29Z","class":"engineering","commit":"1187411746c607ece0e2ecb39e1f8fac1cb87aa6","declarations":1969,"fixture_files":21,"holes":3,"own_files":170,"policy":27,"provers":"agda 28, lean 18, rocq 9, isabelle 6, idris2 48, spark 17, smt-atp 31, why3 1, fstar 6, dafny 1, alloy 1, other 4","repo":"hyperpolymath/echidna","status_doc":"docs/PROOF-STATUS.adoc","unsafe":4},{"axioms":0,"censused_at":"2026-11-10T22:02:35Z","class":"theory","commit":"207ccc5191657d5e84bd8b526c2552116f7b865f","declarations":82,"fixture_files":0,"holes":5,"own_files":12,"policy":0,"provers":"agda 2, lean 4, rocq 3, idris2 3","repo":"hyperpolymath/echidnabot","status_doc":"docs/PROOF-STATUS.adoc","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:02:39Z","class":"theory","commit":"03067a67b785bd11a1b788527fdd1d2a69fdcaf0","declarations":1759,"fixture_files":0,"holes":0,"own_files":165,"policy":1,"provers":"agda 163, lean 1, rocq 1","repo":"hyperpolymath/echo-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":5,"censused_at":"2026-11-10T22:03:32Z","class":"theory","commit":"48ea0e4a4461b0c1ae5f44e449dcad90762ec378","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,"censused_at":"2026-11-10T22:03:52Z","class":"engineering","commit":"da7e92957b2fbf781f0a69f4534147491c02cc5c","declarations":121,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/eclexiaiser","status_doc":"","unsafe":0},{"axioms":12,"censused_at":"2026-11-10T22:03:58Z","class":"engineering","commit":"59e0343c538db8130cff5780a3bb6b6b4b81538a","declarations":719,"fixture_files":0,"holes":0,"own_files":48,"policy":0,"provers":"rocq 24, idris2 24","repo":"hyperpolymath/ephapax","status_doc":"formal/PROOF-STATUS.a2ml","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:04:21Z","class":"engineering","commit":"f35af47e7c33e29f0f8461b944809abdb6cfa43b","declarations":133,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ephapaxiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:25Z","class":"theory","commit":"bfcee6e235dd8802e301ea92fa0d445b1c94b807","declarations":513,"fixture_files":28,"holes":0,"own_files":60,"policy":0,"provers":"agda 60","repo":"hyperpolymath/epistemic-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:48Z","class":"engineering","commit":"bc393f8e9f61df0dae448f046b1544a5218d1a16","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,"censused_at":"2026-11-13T18:29:28Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","declarations":236,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/ExactCounts.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-13T18:29:34Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:04:57Z","class":"engineering","commit":"c0b8767082b67044d291306d668b8cb2e8510dfa","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,"censused_at":"2026-11-10T22:04:59Z","class":"engineering","commit":"25d5aa7554908fbc7d5d5013fdde761b7675da8c","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,"censused_at":"2026-11-10T22:05:01Z","class":"engineering","commit":"413f8a08c808ecefe10de4496679676da62098f4","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,"censused_at":"2026-11-10T22:05:09Z","class":"engineering","commit":"8cc53f2d4bb204cb75f3bc4a651799328d8c2d0e","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,"censused_at":"2026-11-10T22:05:17Z","class":"theory","commit":"034d50ce2dae302ea4b58789833614a90a360598","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,"censused_at":"2026-11-10T22:05:31Z","class":"engineering","commit":"7d974119e263390ace42b8d2a0f585f6b8e289c0","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/flatracoon","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:36Z","class":"engineering","commit":"7caf52310615f71528c30a48c6829bf0c317b3da","declarations":0,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"spark 5, other 1","repo":"hyperpolymath/formatrix-docs","status_doc":"PROOF-NEEDS.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:52Z","class":"engineering","commit":"64ea085964818dce3fa2c2b5252821baa6287618","declarations":136,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/futharkiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:05:57Z","class":"engineering","commit":"ffa76ec2c17ac0d01edcbad5e5d3878242471023","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,"censused_at":"2026-11-10T22:06:01Z","class":"theory","commit":"da29c69f1cb82397d2f3e776a853945de6b067dd","declarations":82,"fixture_files":3,"holes":5,"own_files":15,"policy":0,"provers":"agda 2, lean 4, rocq 3, idris2 6","repo":"hyperpolymath/gitbot-fleet","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:15Z","class":"engineering","commit":"50732be0eeaac30bc163b0f2937c1c5afeff38f8","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/glyphbase","status_doc":"","unsafe":0},{"axioms":7,"censused_at":"2026-11-10T22:06:17Z","class":"theory","commit":"bbed3a0c5e314f1a4be28342440dd3aa7323025d","declarations":737,"fixture_files":8,"holes":4,"own_files":53,"policy":0,"provers":"lean 49, idris2 4","repo":"hyperpolymath/gnpl","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:39Z","class":"engineering","commit":"7083d1934dd945482883e66fae47733afbb95409","declarations":10,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/haec","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:45Z","class":"engineering","commit":"da63c6702f9f1d8ca4473dd7e7eb0e25c54f2d5a","declarations":161,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/halideiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:49Z","class":"engineering","commit":"2aa57e653b397f496ddc87258fe81a2710f90b83","declarations":9,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/hermeneia","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:06:55Z","class":"engineering","commit":"79e784f958e3c57f4cb3f2c6dd3504b3780a27bb","declarations":16,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/heron-polyfeed-reader","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:07:11Z","class":"engineering","commit":"73be9e7eb9c53eaa5207ef70fc75aeef6d3093b1","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,"censused_at":"2026-11-10T22:07:13Z","class":"engineering","commit":"3c00497ee51703c826a85b7aa06fe16547e02d4c","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,"censused_at":"2026-11-10T22:07:14Z","class":"engineering","commit":"c5bb4ffedcd46c85fc04f5511b4fa31122117926","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,"censused_at":"2026-11-10T22:07:16Z","class":"engineering","commit":"14b32c1c302593fe475205e0a90f55a4a97da7b3","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,"censused_at":"2026-11-10T22:07:17Z","class":"engineering","commit":"0f5d47be83fe818ef714d4e6109dbd8069df3d29","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,"censused_at":"2026-11-10T22:07:19Z","class":"engineering","commit":"871dbf1a77cbe6f6fd3eb7b703e98649a710b0d4","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,"censused_at":"2026-11-10T22:07:26Z","class":"engineering","commit":"2ee6ae098f52bd1e0ea97d7d394fa441c25494e2","declarations":680,"fixture_files":24,"holes":3,"own_files":58,"policy":1,"provers":"agda 2, lean 1, rocq 1, idris2 52, tla 2","repo":"hyperpolymath/hypatia","status_doc":"verification/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:07:54Z","class":"engineering","commit":"439f5211635b0f1cceed7058f72a6554da53ad05","declarations":47,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/i-human","status_doc":"","unsafe":0},{"axioms":7,"censused_at":"2026-11-10T22:07:56Z","class":"engineering","commit":"00141a874aefbafa7f175027349cd377623065f0","declarations":77,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/ideas-to-alphas","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:03Z","class":"engineering","commit":"bb9320f7d84e517e23b1fc13ef3ecbe261bfdac0","declarations":122,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/idrisiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:11Z","class":"engineering","commit":"dae1632db8389dad129a1efedb7eb4afad5a76ef","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,"censused_at":"2026-11-10T22:08:15Z","class":"theory","commit":"3a0a8fce3ee95af7e6cc6e6893c0725bf2a25aaf","declarations":16,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/invariant-path","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:17Z","class":"engineering","commit":"843255953c97cf5401118b84344cffb0751e6de3","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,"censused_at":"2026-11-10T22:08:24Z","class":"engineering","commit":"176fa8952e770f1b44a92a2bf98418d65f6ede96","declarations":254,"fixture_files":0,"holes":0,"own_files":18,"policy":0,"provers":"idris2 18","repo":"hyperpolymath/iseriser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:36Z","class":"theory","commit":"12681e2f85226475c7e0e4e79013e7b361eb205a","declarations":223,"fixture_files":12,"holes":0,"own_files":23,"policy":0,"provers":"agda 11, lean 2, rocq 2, idris2 8","repo":"hyperpolymath/januskey","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:08:51Z","class":"theory","commit":"499038a160a86b9528ccc9c3946ef48659ed9d48","declarations":301,"fixture_files":0,"holes":0,"own_files":16,"policy":0,"provers":"agda 5, lean 10, idris2 1","repo":"hyperpolymath/jtv-lang","status_doc":"verification/PROOF-STATUS.adoc","unsafe":0},{"axioms":9,"censused_at":"2026-11-10T22:08:59Z","class":"engineering","commit":"d5aa02993c04cf7428a1ed60baa91e0c0f673275","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,"censused_at":"2026-11-10T22:09:06Z","class":"engineering","commit":"be909895e9355d6137b1911802b746b8220d50d6","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,"censused_at":"2026-11-10T22:09:08Z","class":"engineering","commit":"19899b48f6cf322d0b5c0667f2c41b22467fae23","declarations":140,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/julianiser","status_doc":"","unsafe":0},{"axioms":1,"censused_at":"2026-11-13T18:29:37Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"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,"censused_at":"2026-11-10T22:09:11Z","class":"engineering","commit":"20f6be5b5a14a48680b236955b5c4ad9033d00d4","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,"censused_at":"2026-11-10T22:09:15Z","class":"engineering","commit":"ef018acb4381f7cbf81a98c5c1dbc05d299fe985","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,"censused_at":"2026-11-10T22:09:17Z","class":"engineering","commit":"948d020226b3110b6792facf856b88c2bc4d8788","declarations":105,"fixture_files":0,"holes":1,"own_files":13,"policy":0,"provers":"idris2 13","repo":"hyperpolymath/kategoria","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":4,"censused_at":"2026-11-10T22:09:24Z","class":"engineering","commit":"ff7ddde1c9fc9161ee031afad6e802aa24940247","declarations":111,"fixture_files":0,"holes":0,"own_files":11,"policy":1,"provers":"agda 5, idris2 6","repo":"hyperpolymath/kitchenspeak","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:09:32Z","class":"engineering","commit":"6f085752c790bbba91e5fa0110a304ea316daa8c","declarations":61,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"agda 2, idris2 3","repo":"hyperpolymath/krl","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:09:36Z","class":"engineering","commit":"7fc73e85e213d94539d3ea00adcd18ccd908180f","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,"censused_at":"2026-11-10T22:09:37Z","class":"engineering","commit":"8207b18d2a36fe19400540481b3b4cdb766c2321","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,"censused_at":"2026-11-10T22:09:40Z","class":"engineering","commit":"b64e5cdda1680432793ee167759fd2aa7bcdeb65","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,"censused_at":"2026-11-10T22:09:50Z","class":"theory","commit":"ca03e7c2b7c93be3057ed308c6c129e056a9edf0","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-STATUS.adoc","unsafe":0},{"axioms":2,"censused_at":"2026-11-10T22:10:08Z","class":"engineering","commit":"b873cefb7161df945535a0a20e19b312cb7f53da","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,"censused_at":"2026-11-10T22:10:18Z","class":"engineering","commit":"392f77ff03b92849940e31b0d965e977bcd0605d","declarations":141,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/lustreiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:10:22Z","class":"engineering","commit":"314750d03ec580e2404c70173ac0a0f6f5ea86be","declarations":11,"fixture_files":1,"holes":0,"own_files":8,"policy":2,"provers":"agda 3, spark 3, other 2","repo":"hyperpolymath/maa-framework","status_doc":"docs/proof-debt.adoc","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:10:27Z","class":"theory","commit":"e479ebc2319438a5db6b8b3f3d8f1a4749014747","declarations":198,"fixture_files":0,"holes":0,"own_files":17,"policy":0,"provers":"lean 17","repo":"hyperpolymath/marches","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:10:34Z","class":"theory","commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","declarations":51,"fixture_files":0,"holes":0,"own_files":6,"policy":1,"provers":"agda 2, lean 3, rocq 1","repo":"hyperpolymath/mathesis","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:40:18Z","class":"theory","commit":"4dbd1adc08e50fb526eb756519634e67c63ac492","declarations":107,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"agda 13","repo":"hyperpolymath/MetaManifold-WebUI","status_doc":"proofs/PROOF-STATUS.md","unsafe":0},{"axioms":26,"censused_at":"2026-11-10T22:10:57Z","class":"theory","commit":"0ba3b9fb0397c2142ea3883330508caa871259e1","declarations":617,"fixture_files":0,"holes":0,"own_files":25,"policy":0,"provers":"rocq 16, idris2 9","repo":"hyperpolymath/my-lang","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:24Z","class":"engineering","commit":"8a6663416f95c20eeeb4fb6401572b18132e1400","declarations":135,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/mylangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:34Z","class":"engineering","commit":"65e6a3029dfb53be3d731df18f256d566fa90fef","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,"censused_at":"2026-11-10T22:11:35Z","class":"engineering","commit":"c5a0bc5466dc724142003779548024d2acf8a941","declarations":0,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"spark 3, other 1","repo":"hyperpolymath/network-ambulance","status_doc":"","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:11:40Z","class":"theory","commit":"49cf1bce1d571f6683e3631f950a1bbb170b78fe","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,"censused_at":"2026-11-10T22:11:47Z","class":"engineering","commit":"4cf7548cd4ce243ab1688710e2540431e74b9442","declarations":279,"fixture_files":3,"holes":0,"own_files":24,"policy":0,"provers":"idris2 24","repo":"hyperpolymath/nextgen-databases","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:55Z","class":"engineering","commit":"21cd89b9f1db1cf3cd1977418eba65a96077eb09","declarations":15,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/nextgen-language-evangeliser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:11:57Z","class":"theory","commit":"bc91959b41b54043deb2e5776d322bb822990ccc","declarations":118,"fixture_files":11,"holes":4,"own_files":16,"policy":0,"provers":"agda 3, lean 6, rocq 7","repo":"hyperpolymath/nextgen-typing","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:03Z","class":"engineering","commit":"658f28e28fead22987e4c440db787c584678e296","declarations":147,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/nimiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:08Z","class":"engineering","commit":"6739b86bae506a7653155ea22e08f200874bb5cd","declarations":156,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/oblibeniser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:12Z","class":"engineering","commit":"c76df124ddb47f18b02377acadae339c0386aea8","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,"censused_at":"2026-11-10T22:12:16Z","class":"theory","commit":"1ba67f7768b7e6020df050fdbf5bee7920b68630","declarations":90,"fixture_files":2,"holes":0,"own_files":20,"policy":0,"provers":"agda 8, lean 6, idris2 6","repo":"hyperpolymath/occupancy-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:12:30Z","class":"engineering","commit":"aab2fa3bde65a413dcbb8a75064fd063a9bed2c0","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,"censused_at":"2026-11-10T22:12:51Z","class":"engineering","commit":"62f1b8554611e13a87447e6d401c89e997bbe292","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,"censused_at":"2026-11-10T22:12:56Z","class":"engineering","commit":"739d7cbc339ccee76e694520f5a201a3acb142c5","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":2,"censused_at":"2026-11-10T22:13:08Z","class":"theory","commit":"f27d2921c2a577b43306d82fc6a2b42dc0b19447","declarations":625,"fixture_files":0,"holes":0,"own_files":78,"policy":1,"provers":"agda 78","repo":"hyperpolymath/ordinal-notation","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:36Z","class":"engineering","commit":"fa39db2edf79eba611169d91671d9751c3e1d1ec","declarations":157,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/otpiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:40Z","class":"theory","commit":"21be6420f4aa4c2486488b5c8e4031be42384d76","declarations":43,"fixture_files":4,"holes":0,"own_files":7,"policy":0,"provers":"agda 5, lean 1, rocq 1","repo":"hyperpolymath/palimpsest-license","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:45Z","class":"engineering","commit":"15868fee549383c063a4efcf8eaaa75616189943","declarations":65,"fixture_files":1,"holes":0,"own_files":14,"policy":0,"provers":"idris2 5, tla 9","repo":"hyperpolymath/panic-attack","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:51Z","class":"engineering","commit":"d142b63856559e30c134e6d70e4779b9132dd6ae","declarations":169,"fixture_files":11,"holes":0,"own_files":21,"policy":0,"provers":"idris2 17, tla 4","repo":"hyperpolymath/panll","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:13:59Z","class":"engineering","commit":"2e40cac9e7df54654edcfae9d92a723427d35175","declarations":14,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/panoply","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:03Z","class":"engineering","commit":"c12e76f862c4ea5e85e7c3a283b1372cf0dc37c7","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,"censused_at":"2026-11-10T22:14:10Z","class":"engineering","commit":"c659474f807f0f187c33a99f782a91b03ecac16b","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,"censused_at":"2026-11-10T22:14:12Z","class":"engineering","commit":"a62fd06ab828dce790704e98885cf8e55dc2577c","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,"censused_at":"2026-11-10T22:14:14Z","class":"theory","commit":"b06a951820feb0b99731d85627057915873edeae","declarations":140,"fixture_files":0,"holes":0,"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,"censused_at":"2026-11-10T22:14:20Z","class":"engineering","commit":"6b2b2f6b06a5741c9400162e86978292ec07c9a7","declarations":155,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/phronesiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:23Z","class":"engineering","commit":"b5193824d5638e0dbcd9489a8aa619928e2c9dad","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,"censused_at":"2026-11-10T22:14:29Z","class":"engineering","commit":"5d05ebf85af03ced28c44fb778029923acf3813f","declarations":44,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"idris2 2, spark 4, other 1","repo":"hyperpolymath/poly-ssg","status_doc":"","unsafe":1},{"axioms":0,"censused_at":"2026-11-10T22:14:32Z","class":"engineering","commit":"31f57c30ae577f96540b3c00d49e9b90b4cd3761","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,"censused_at":"2026-11-10T22:14:34Z","class":"engineering","commit":"db0907c0d0b3fd437a58648573bb4fdf9e43178d","declarations":0,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"spark 4, other 1","repo":"hyperpolymath/polyglot-i18n","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:45Z","class":"engineering","commit":"9f0926715bb5d3b42f0290a46c163cfd1f07615a","declarations":137,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/ponyiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:49Z","class":"engineering","commit":"52326c5039e9fbeacb7491ab23fde40fc32c38d5","declarations":76,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 6","repo":"hyperpolymath/presswerk","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:14:57Z","class":"theory","commit":"75575b27a51b634f8d0ab3845f0fd94930e6177b","declarations":31,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"hyperpolymath/proof-burrower","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":2,"censused_at":"2026-11-10T22:15:04Z","class":"theory","commit":"3d50aa044666c5a0c6ea722231e2bb55e69740a1","declarations":365,"fixture_files":0,"holes":0,"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":368,"censused_at":"2026-11-10T22:15:30Z","class":"engineering","commit":"a7503b2d96c4e292d8a3239304e187a5c31bc4e6","declarations":11166,"fixture_files":60,"holes":22,"own_files":927,"policy":0,"provers":"lean 14, idris2 906, spark 2, tla 1, other 4","repo":"hyperpolymath/proven","status_doc":"docs/proof-debt-triage-tier-a.adoc","unsafe":10},{"axioms":0,"censused_at":"2026-11-10T22:20:40Z","class":"engineering","commit":"24b244ac9c8e51341139cf5e69c27a19bd154645","declarations":47,"fixture_files":1,"holes":0,"own_files":7,"policy":0,"provers":"idris2 6, creusot 1","repo":"hyperpolymath/proven-cicd-and-workflows","status_doc":"","unsafe":0},{"axioms":3,"censused_at":"2026-11-10T22:20:43Z","class":"engineering","commit":"ebc440f3a865565faf95c911a4df04351213dab5","declarations":6242,"fixture_files":0,"holes":3,"own_files":899,"policy":0,"provers":"idris2 899","repo":"hyperpolymath/proven-servers","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:11Z","class":"engineering","commit":"f90bacbe3a5fa1869239fcb9175757509464aa13","declarations":891,"fixture_files":29,"holes":0,"own_files":75,"policy":0,"provers":"idris2 75","repo":"hyperpolymath/proven-tests-and-benches","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:37Z","class":"engineering","commit":"bc45e1a0d34fad39b2717819c5a52da688bb5aae","declarations":12,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/puggle","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:43Z","class":"engineering","commit":"68c1485f0e33dfddc0478618c69bf87454307c87","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,"censused_at":"2026-11-10T22:26:46Z","class":"engineering","commit":"68b7a4ccd035833e68b34f562c3fd965a2f389f6","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:26:56Z","class":"engineering","commit":"5ebbdc2fcad9e21e42f1b5f1c42a98e3345511f7","declarations":59,"fixture_files":0,"holes":0,"own_files":17,"policy":0,"provers":"idris2 3, spark 13, other 1","repo":"hyperpolymath/raze-tui","status_doc":"","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:27:04Z","class":"engineering","commit":"7464e6ba60e63901ec04e76e069007d925789595","declarations":25,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"hyperpolymath/recon-silly-ation","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:27:19Z","class":"engineering","commit":"a04b755e70761a0b55a77cf03903bcd642a15258","declarations":7,"fixture_files":0,"holes":0,"own_files":5,"policy":0,"provers":"idris2 1, spark 2, other 2","repo":"hyperpolymath/reposystem","status_doc":"PROOF-NEEDS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:27:39Z","class":"theory","commit":"6f94640d370f3470bfbc59f76fa233ee5e9f92b0","declarations":391,"fixture_files":23,"holes":0,"own_files":37,"policy":0,"provers":"agda 37","repo":"hyperpolymath/residual-evidence-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T21:48:16Z","class":"theory","commit":"a92a9e2fd5f0b43d0209ad92f1076aef2bddf520","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,"censused_at":"2026-11-10T22:27:51Z","class":"theory","commit":"a19a5b8d0ad742aa49c9d19e4312c481972d95c1","declarations":467,"fixture_files":12,"holes":0,"own_files":25,"policy":0,"provers":"agda 22, lean 2, rocq 1","repo":"hyperpolymath/resource-algebra","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:28:10Z","class":"engineering","commit":"d94110acfec2b6b0cfc8566594d9bf0a89da33d0","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,"censused_at":"2026-11-10T22:28:16Z","class":"engineering","commit":"3341a1de656eb1657cddcc5c081933fb10549148","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,"censused_at":"2026-11-10T22:28:50Z","class":"engineering","commit":"0dfde85e6745d1f56a22cf49e11a74abb97b4dd5","declarations":136,"fixture_files":0,"holes":0,"own_files":18,"policy":1,"provers":"agda 1, lean 2, rocq 1, idris2 11, tla 3","repo":"hyperpolymath/rsr-template-repo","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:08Z","class":"theory","commit":"c9c4b3995941aa27d51bc5e68ecb67fdafc673fc","declarations":304,"fixture_files":6,"holes":0,"own_files":30,"policy":0,"provers":"agda 22, lean 7, rocq 1","repo":"hyperpolymath/secret-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:23Z","class":"engineering","commit":"ccdba3cca5f928c7e94f13b551c684a5b3a64dd9","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,"censused_at":"2026-11-10T21:48:22Z","class":"engineering","commit":"84b6e3644840233c02e660612fccc539cb66ddd2","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/SMTLib.jl","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:30Z","class":"engineering","commit":"76a661998aea8d9e198ddf368e618fe9ac7d0c01","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,"censused_at":"2026-11-10T22:29:33Z","class":"engineering","commit":"720eb82168adb0947ab624a7e27972c7c7c9f9d6","declarations":223,"fixture_files":0,"holes":0,"own_files":13,"policy":1,"provers":"agda 3, lean 1, rocq 1, idris2 7, tla 1","repo":"hyperpolymath/snifs","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:29:47Z","class":"engineering","commit":"4abaef5c2607787d6b01b0c06e6e940c60d9bb6c","declarations":0,"fixture_files":0,"holes":0,"own_files":7,"policy":0,"provers":"spark 6, other 1","repo":"hyperpolymath/somethings-fishy","status_doc":"PROOF-STATUS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:29:58Z","class":"engineering","commit":"e5b7e7fd9af511a1c339cfbd2824e0cccd03fada","declarations":108,"fixture_files":0,"holes":3,"own_files":18,"policy":0,"provers":"lean 1, idris2 6, spark 8, other 3","repo":"hyperpolymath/ssg-collection","status_doc":"PROOF-NEEDS.adoc","unsafe":2},{"axioms":0,"censused_at":"2026-11-10T22:30:05Z","class":"engineering","commit":"077cc55ad239c824ca65923b0924105ab0d94c60","declarations":56,"fixture_files":0,"holes":0,"own_files":6,"policy":0,"provers":"idris2 4, tla 2","repo":"hyperpolymath/stateful-artefacts","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:30:10Z","class":"theory","commit":"f2de559f2be33c4a81e2550aa6b75ac1689c7bf8","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,"censused_at":"2026-11-10T22:30:13Z","class":"theory","commit":"126a3b86636de66be3c5811ff3a278c61f887b8e","declarations":773,"fixture_files":0,"holes":0,"own_files":102,"policy":0,"provers":"agda 80, lean 22","repo":"hyperpolymath/system-et","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:30:44Z","class":"theory","commit":"6f070d6eb3faaac75acc6fb2f667e81d43effef2","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,"censused_at":"2026-11-10T22:30:50Z","class":"engineering","commit":"a33a1e79864f6c2725cb8e03dd9134df8c5d2c1a","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,"censused_at":"2026-11-10T22:30:53Z","class":"engineering","commit":"e188f42aab2e24758e487516e3e9c107c8947262","declarations":181,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/tlaiser","status_doc":"","unsafe":0},{"axioms":23,"censused_at":"2026-11-10T22:31:04Z","class":"engineering","commit":"a5163f5145c1ff0add007c35cb15aba6b64a7c93","declarations":165,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"agda 2, idris2 5, spark 1, other 1","repo":"hyperpolymath/trigger","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:23Z","class":"theory","commit":"24d1985fd16e5af9baaa854f1496a7067b278a05","declarations":514,"fixture_files":0,"holes":0,"own_files":38,"policy":1,"provers":"agda 10, lean 12, idris2 16","repo":"hyperpolymath/trope-checker","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:38Z","class":"theory","commit":"f2e465c966d14d4986dfc492875cc54653d9751e","declarations":564,"fixture_files":0,"holes":4,"own_files":29,"policy":0,"provers":"lean 20, isabelle 9","repo":"hyperpolymath/tropical-types","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:31:48Z","class":"engineering","commit":"a86bba4100d3f27919a154cdefeee60ef64cb5a8","declarations":896,"fixture_files":17,"holes":0,"own_files":52,"policy":0,"provers":"idris2 52","repo":"hyperpolymath/typed-wasm","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:32:05Z","class":"engineering","commit":"aa42bb15d9a2e9363f63dba2815c7d733c13da41","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,"censused_at":"2026-11-10T22:32:11Z","class":"engineering","commit":"5a6592aecca77e90b7d9aced9496ab8eddb5c81f","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,"censused_at":"2026-11-10T22:32:20Z","class":"engineering","commit":"549e08fb25146128f84beebbfbc873456f064a19","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,"censused_at":"2026-11-10T22:32:23Z","class":"engineering","commit":"ba91e87607724066029855dba43b326c2e095a43","declarations":28,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"hyperpolymath/unified-api-adapter","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:32:29Z","class":"engineering","commit":"56ad8091601b19a211967812b8a7209c32d0020d","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,"censused_at":"2026-11-10T22:32:31Z","class":"engineering","commit":"b8b6f99290e16a1ed0a55c73b8ceabaa3223fb25","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,"censused_at":"2026-11-10T22:32:35Z","class":"engineering","commit":"fc3b6da2446a4755745a33acfe34c6a37a2b00ae","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,"censused_at":"2026-11-10T22:32:38Z","class":"engineering","commit":"dd4e6c87c08402e430f6d7f19c9c58d35db31ed6","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":0,"censused_at":"2026-11-10T22:32:39Z","class":"theory","commit":"48a88eaa58b0c8121fb15a575f263b5a432fad1a","declarations":1031,"fixture_files":0,"holes":5,"own_files":68,"policy":0,"provers":"agda 12, lean 17, rocq 12, isabelle 9, idris2 12, dedukti 1, smt-atp 5","repo":"hyperpolymath/valence-shell","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:04Z","class":"engineering","commit":"5b10cb01ef1b1b5e1b6568a53c2d63c1fa959a81","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,"censused_at":"2026-11-10T22:33:24Z","class":"engineering","commit":"c67b2c33d4a29d96cda30db79af641e99ce175fc","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,"censused_at":"2026-11-10T22:33:30Z","class":"engineering","commit":"703961842e614a7a6760e087cb3dbf5fc855c1c0","declarations":424,"fixture_files":0,"holes":3,"own_files":21,"policy":0,"provers":"rocq 10, idris2 11","repo":"hyperpolymath/verisimdb","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:44Z","class":"engineering","commit":"9633e0113fa3e831c51684965195aa2bf84b9766","declarations":208,"fixture_files":0,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"hyperpolymath/verisimiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:33:51Z","class":"engineering","commit":"9d1002f60fda57293cfa00cd85869aae60a8071a","declarations":104,"fixture_files":0,"holes":3,"own_files":10,"policy":0,"provers":"idris2 10","repo":"hyperpolymath/vexometer","status_doc":"PROOF-NEEDS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:11Z","class":"engineering","commit":"7fb6c9fa37086b597df380e20a13aa99dbe898af","declarations":58,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/volumod","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:12Z","class":"engineering","commit":"acf709911e868c6308c4b51647c8b4f4f23c42da","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,"censused_at":"2026-11-10T22:34:14Z","class":"theory","commit":"1624f4187f62eed7df026795fce628bfff2689bf","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,"censused_at":"2026-11-10T22:34:22Z","class":"engineering","commit":"8db48b2e4aba9756bd92ce3c81cfdea692a1f504","declarations":143,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"idris2 9","repo":"hyperpolymath/wokelangiser","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:34:36Z","class":"theory","commit":"2b5ddcc0003f44329222ff88072b0241d368ff02","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,"censused_at":"2026-11-10T22:34:38Z","class":"engineering","commit":"7a37073dfba0cb1ef126113dab8069be52370a12","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,"censused_at":"2026-11-10T22:34:48Z","class":"engineering","commit":"b4d7c252bae52b1698c5a3168a4dc56f57f9fee9","declarations":110,"fixture_files":0,"holes":0,"own_files":8,"policy":0,"provers":"agda 1, lean 1, rocq 1, idris2 5","repo":"hyperpolymath/zig-dnssec","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:35:06Z","class":"theory","commit":"a8b4be7fb3273327d81cd84dd3fe9984d336001c","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,"censused_at":"2026-11-10T22:35:35Z","class":"engineering","commit":"aa3ef263ac6ac177a5b0c6fa33e5814c8589101a","declarations":70,"fixture_files":0,"holes":3,"own_files":5,"policy":0,"provers":"idris2 5","repo":"metadatastician/_pathroot","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:35:51Z","class":"engineering","commit":"57b617c7a0a4940f0458f2516e66c69291a0e88a","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,"censused_at":"2026-11-10T22:36:03Z","class":"engineering","commit":"692976054f11764d8daa8736d6e091ed075a2737","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/bowtie-workbench","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:08Z","class":"engineering","commit":"3da26e6c65a1cbcf90ae006e0a2971ce03228641","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,"censused_at":"2026-11-10T22:36:15Z","class":"engineering","commit":"738b209a9370aef3c693801b887709d671827d3b","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/cadastra","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:20Z","class":"engineering","commit":"e8dc1b724a3e47e6a1563a99f715e4252a38f6d5","declarations":91,"fixture_files":0,"holes":18,"own_files":38,"policy":0,"provers":"idris2 8, spark 28, other 2","repo":"metadatastician/cerro-torre","status_doc":"","unsafe":69},{"axioms":0,"censused_at":"2026-11-10T22:36:47Z","class":"engineering","commit":"7a3ba13b808e590c64859e866fae0f6d316cbca8","declarations":38,"fixture_files":3,"holes":0,"own_files":12,"policy":0,"provers":"idris2 12","repo":"metadatastician/cleave","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:51Z","class":"engineering","commit":"e3d349616ddc48da52b42e606fe36ac1f2f9207a","declarations":27,"fixture_files":0,"holes":0,"own_files":4,"policy":0,"provers":"idris2 4","repo":"metadatastician/common-signal","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:36:58Z","class":"engineering","commit":"0e033878078bb11136e7459e2f34cbc0b6c0d6f6","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/first-post","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:37:09Z","class":"engineering","commit":"37a3ad5ac3a19378c84fffc446939954a5d9dd79","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,"censused_at":"2026-11-10T22:37:28Z","class":"engineering","commit":"a8534de4e438e108af0f6f86c802fcef64856d64","declarations":185,"fixture_files":3,"holes":0,"own_files":19,"policy":0,"provers":"idris2 19","repo":"metadatastician/groove","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:37:36Z","class":"theory","commit":"da01ab82aa6b1974276e6f7f064c2beed2f356b4","declarations":640,"fixture_files":7,"holes":0,"own_files":19,"policy":0,"provers":"agda 10, lean 1, rocq 1, idris2 1, tla 6","repo":"metadatastician/hvn-dehallucinator","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:18Z","class":"engineering","commit":"9175fe1971b55e37a9b4c27f3b77b1a40f93b46e","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,"censused_at":"2026-11-10T22:38:26Z","class":"theory","commit":"89ceac3b8685467c664737a98364eef4febb9ff2","declarations":240,"fixture_files":9,"holes":0,"own_files":21,"policy":0,"provers":"agda 13, lean 7, rocq 1","repo":"metadatastician/lintel","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:38Z","class":"engineering","commit":"e5f30dfd891e66c235c6d8c52997a330750c2f1f","declarations":0,"fixture_files":0,"holes":0,"own_files":1,"policy":0,"provers":"idris2 1","repo":"metadatastician/marid","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0},{"axioms":1,"censused_at":"2026-11-10T22:35:13Z","class":"theory","commit":"5cd0c90498384f6f465278a7a3d1a074cd78b45f","declarations":341,"fixture_files":0,"holes":0,"own_files":49,"policy":0,"provers":"agda 13, lean 18, rocq 18","repo":"metadatastician/MetaManifold-Evidence","status_doc":"PROOF-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:38:51Z","class":"engineering","commit":"b161660e6b18c9f5b58dceae156fbc4930da92e1","declarations":1149,"fixture_files":8,"holes":4,"own_files":64,"policy":3,"provers":"agda 3, lean 2, rocq 1, idris2 51, tla 7","repo":"metadatastician/paint-type","status_doc":"PROOF-STATUS.adoc","unsafe":8},{"axioms":4,"censused_at":"2026-11-10T22:39:12Z","class":"engineering","commit":"45a86eb761537785ee019315b5ed3148a71b7d17","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,"censused_at":"2026-11-10T22:39:16Z","class":"engineering","commit":"c9f5fce6f18454510ca016608748aa834f1801cd","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,"censused_at":"2026-11-10T22:39:18Z","class":"engineering","commit":"4a6e86cd6417274d9f44c8ac37ceedcd06567446","declarations":23,"fixture_files":0,"holes":4,"own_files":2,"policy":0,"provers":"idris2 2","repo":"metadatastician/selur","status_doc":"","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:21Z","class":"engineering","commit":"3804c2071d43213ac935733bda826629fbbe46cf","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-STATUS.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:28Z","class":"engineering","commit":"d73229d8220a35f66e99678966797dd6399dda1f","declarations":40,"fixture_files":0,"holes":0,"own_files":2,"policy":0,"provers":"idris2 2","repo":"metadatastician/standards","status_doc":"docs/proof-debt.adoc","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:35Z","class":"engineering","commit":"9858bf0ca5f9bd5c332b24403229da08daa478c9","declarations":294,"fixture_files":8,"holes":0,"own_files":19,"policy":0,"provers":"idris2 18, alloy 1","repo":"metadatastician/stapeln","status_doc":"docs/proof-debt.md","unsafe":0},{"axioms":0,"censused_at":"2026-11-10T22:39:47Z","class":"engineering","commit":"017616c5e31db41c9bd667d2aa35298cab8b81ab","declarations":129,"fixture_files":2,"holes":0,"own_files":26,"policy":0,"provers":"idris2 10, spark 12, creusot 2, verus 1, other 1","repo":"metadatastician/vordr","status_doc":"","unsafe":4},{"axioms":0,"censused_at":"2026-11-10T22:35:29Z","class":"theory","commit":"add77b1edbfd7fc37a25c05e9c08f06af6567756","declarations":53,"fixture_files":0,"holes":0,"own_files":3,"policy":0,"provers":"agda 3","repo":"metadatastician/ZenodoDeposits.jl","status_doc":"docs/status/PROOF-STATUS.adoc","unsafe":0}],"schema":"mathesis.census-atlas/0.1","source":"docs/atlas/census/rows.jsonl","verification":"not_asserted"}
diff --git a/scripts/census/proof-holes.sh b/scripts/census/proof-holes.sh
index 5d1eea5..08d2fda 100644
--- a/scripts/census/proof-holes.sh
+++ b/scripts/census/proof-holes.sh
@@ -11,6 +11,12 @@
 #   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)
+#   control a finding inside a declared negative control: a file whose own header
+#           carries a line comment `EXPECT: <pattern>`, the home repository's
+#           statement that the checker must reject it for that reason (for
+#           example CompositionalDA.jl proofs/agda/reject/). It is reported, not
+#           dropped, but it is not a hole, axiom, unsafe or policy count and does
+#           not affect --fail-on: the home gate is what rejects it.
 #
 # This is a textual scan: it finds candidates, it does not decide them. A
 # kernel-level audit (#print axioms, Print Assumptions, gnatprove report,
@@ -34,7 +40,7 @@ while [ $# -gt 0 ]; do
     --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 ;;
+    -h|--help) sed -n '3,28p' "$0"; exit 0 ;;
     -*) echo "unknown option: $1" >&2; exit 2 ;;
     *) DIR=$1; shift ;;
   esac
@@ -96,9 +102,17 @@ 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" \
+# A negative control declares itself: a line comment `EXPECT: <pattern>` in the
+# file names the error the home gate expects when it rejects the file.
+is_control() {
+  local path=$1
+  grep -qE '^[[:space:]]*(--|//|#)[[:space:]]*EXPECT:[[:space:]]*[^[:space:]]' "$path" 2>/dev/null
+}
+emit() {
+  local lang=$1 class=$2 marker=$3 file=$4 line=$5 text=$6
+  if [[ $class != control ]] && is_control "$DIR/$file"; then class=control; fi
+  jq -cnS --arg lang "$lang" --arg class "$class" --arg marker "$marker" --arg file "$file" \
+        --argjson line "$line" --arg text "$text" \
         '{lang:$lang,class:$class,marker:$marker,file:$file,line:$line,text:$text}'
 }
 
@@ -211,7 +225,10 @@ 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"; }
+count() {
+  local wanted=$1
+  jq -s --arg c "$wanted" '[.[] | select(.class!="control" and ($c=="any" or .class==$c))] | length' "$OUT"
+}
 case "$FAIL_ON" in
   none) exit 0 ;;
   hole) [ "$(count hole)" -eq 0 ] ;;
diff --git a/scripts/census/summarise.sh b/scripts/census/summarise.sh
index e13c0b1..f8d21ce 100644
--- a/scripts/census/summarise.sh
+++ b/scripts/census/summarise.sh
@@ -53,7 +53,7 @@ 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 "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), control = a finding inside a declared negative control (a file whose header has an EXPECT: line; reported, not counted)."
 echo
 echo "## Repos with artefacts (sorted by declarations)"
 echo
diff --git a/tests/census/proof_holes_control_test.sh b/tests/census/proof_holes_control_test.sh
new file mode 100644
index 0000000..981b25b
--- /dev/null
+++ b/tests/census/proof_holes_control_test.sh
@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# A file that declares itself a negative control (a header line comment
+# `EXPECT: <pattern>`, as in CompositionalDA.jl proofs/agda/reject/) has its
+# findings reported as class "control", not "axiom"/"policy". The same marker in
+# a file with no EXPECT line is still an axiom, and --fail-on is unaffected by
+# a control. Regression for the CompositionalDA.jl row (axioms 1, 2026-11-10).
+set -euo pipefail
+SCAN="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)/scripts/census/proof-holes.sh"
+F=$(mktemp -d); trap 'rm -rf "$F"' EXIT
+printf '%s\n' '-- Negative control.' '-- EXPECT: [Pp]ostulate' 'module reject.P where' 'postulate z : Set' > "$F/Control.agda"
+printf '%s\n' '{-# OPTIONS --safe #-}' 'module Real where' 'postulate z : Set' > "$F/Real.agda"
+printf '%s\n' '{-# OPTIONS --safe #-}' 'module Prose where' '-- see EXPECT: in the control' 'postulate y : Set' > "$F/Prose.agda"
+got=$(bash "$SCAN" --fail-on none "$F" | jq -r '"\(.file):\(.line) \(.class) \(.marker)"' | sort)
+want=$(sort <<'WANT'
+Control.agda:1 control no --safe
+Control.agda:4 control postulate
+Prose.agda:4 axiom postulate
+Real.agda:3 axiom postulate
+WANT
+)
+[[ "$got" == "$want" ]] || { echo "FAIL: control classification differs"; diff <(printf '%s\n' "$want") <(printf '%s\n' "$got") || true; exit 1; }
+rm "$F/Real.agda" "$F/Prose.agda"
+bash "$SCAN" --fail-on any "$F" >/dev/null || { echo "FAIL: a control alone must not fail --fail-on any"; exit 1; }
+echo "PASS: negative-control findings classed control, real and prose-only files still axioms"