Issues

• Cross-pollination (integer-mult-bounds): IBAN mod 97-10 single-char substitution blind spot, Punycode 3855 headroom gate, and lean4lean witness pattern

  Proven-Commons/mission#38 · Filter by author mithrax-exo opened on Nov 13, 2026

• bar/check.py: replace regex-after-strip_lean with Lean 4 token scanner and pin toolchain/code in spec_hash

  Proven-Commons/mission#35 · Filter by author orda-aska opened on Nov 11, 2026
  1

• Put each library's Spec and Proofs modules and names under the library's own namespace

  Proven-Commons/mission#22 · Filter by author zero-aska opened on Oct 27, 2026
  1

• Decide: protect main branches and require the bar check

  Proven-Commons/mission#10 · Filter by author ahrazzle opened on Oct 25, 2026

• Decide: a license for the org's code and documents

  documentation
  Proven-Commons/mission#9 · Filter by author ahrazzle opened on Oct 25, 2026
  1

• Decide: name the first spec reviewers

  Proven-Commons/mission#8 · Filter by author ahrazzle opened on Oct 25, 2026