Issues

• Spec v0.2 review findings deferred to the owner (L3, L6, C2, detect profile, O1-carrier citation)

  enhancementproofstech-debt
  hyperpolymath/trope-checker#106 · Filter by author hyperpolymath opened on Oct 27, 2026
  1

• Two checks red on main for reasons unrelated to any PR: lint-workflows (SPDX must be line 1) and estate-audit (sorry-prose false positives, e2e TODOs)

  cicdlicensingproofstech-debt
  hyperpolymath/trope-checker#105 · Filter by author hyperpolymath opened on Oct 27, 2026

• proofs.yml lean-build is red on main: lean-action's nanoda step cannot build lean4export under the v4.16.0 toolchain

  enhancementproofs
  hyperpolymath/trope-checker#104 · Filter by author hyperpolymath opened on Oct 27, 2026

• just proof-check-all is red: per-file checks resolve no modules; ABI/Types Idris2 mint templates do not typecheck

  hyperpolymath/trope-checker#103 · Filter by author hyperpolymath opened on Oct 27, 2026

• CI: 9 red check(s) on the default branch, deferred from #96

  chorecicd
  hyperpolymath/trope-checker#97 · Filter by author hyperpolymath opened on Oct 1, 2026
  1

• E2E / aspect / benchmark coverage: the workflow was never instantiated (29 repos affected)

  priority:p2scope:estatestatus:blockedtesting
  hyperpolymath/trope-checker#65 · Filter by author hyperpolymath opened on Aug 5, 2026

• CO-1: operational model for fix/lfp — does recursion's grade live in the commutative cost-quotient?

  enhancementhelp wantedpriority:p3scope:repo
  hyperpolymath/trope-checker#10 · Filter by author hyperpolymath opened on Jun 29, 2026
  4