Skip to content

Public description overclaims 'cannot crash / formally verified' vs honest MODULE-STATUS (4 proven, 37 safe-only) #161

Description

@hyperpolymath

Summary

The public GitHub repository description still carries a blanket overclaim that the repo's own internal honesty docs (MODULE-STATUS.txt, PROOF-NEEDS.md) have already retired. Since proven is the estate trust root, the outward-facing claim must match the honest internal ledger.

The mismatch

Current public description:

Code that cannot crash. Formally verified library for safe math, crypto, parsing, and validation. Call from Python, Rust, JavaScript, Go — any language.

What the repo's own MODULE-STATUS.txt (audited 2026-03-29) says:

  • 4 FIRST-CLASS modules contain dependent-type proofs: Core, SafeAttestation, SafeOrdering, SafeTrust.
  • 37 SECOND-CLASS modules — verbatim: "compile and provide safe APIs (returning Maybe/Either instead of crashing) but do NOT contain formal dependent-type proofs. They are useful and correct, but 'safe' not 'proven' in the mathematical sense."
  • Remainder are WIP / not-proven/.

What PROOF-NEEDS.md (honesty refresh 2026-05-18) already states:

  • The earlier framing was "dishonest by a wide margin."
  • "dozens of modules ship verbatim security claims in their doc headers (Prevents:, formally verified, guaranteed, cannot crash) with zero discharged theorem."
  • "proven is the estate trust root, so this ledger must not overclaim."

The internal ledger was fixed; the public-facing description and README headline were not. A visitor (or potential sponsor) sees "Code that cannot crash. Formally verified" before ever reaching the honest status files.

Why this is critical

  • It is the same silent-overclaim class the repo's own adversarial audit flagged — now living in the most-read, least-caveated surface (the repo blurb / social card).
  • It contradicts the estate AFFIRMATION honesty convention. Notably, proven has no AFFIRMATION.adoc, unlike sibling verified repos (echidna, ephapax, typed-wasm).
  • As the trust root, an overclaim here undermines the credibility of every repo that depends on it.

Proposed fix

  1. Rewrite the GitHub description to match MODULE-STATUS.txt. Suggested:

    Multi-language safety library in Idris2: crash-safe wrappers for math, crypto, parsing & validation, with dependent-type proofs for core modules. Honest per-module status in MODULE-STATUS.txt.

  2. Reconcile the README headline the same way — drop the unqualified "Code that cannot crash. Formally verified"; state the FIRST-CLASS vs SECOND-CLASS distinction up front.
  3. Add an AFFIRMATION.adoc (per estate convention) pointing at MODULE-STATUS.txt / PROOF-NEEDS.md as the ground truth.
  4. Audit per-module doc headers for residual formally verified / cannot crash / guaranteed strings on modules with no discharged theorem (PROOF-NEEDS.md already enumerates these).

Evidence

  • MODULE-STATUS.txt — 4 FIRST-CLASS / 37 SECOND-CLASS, audited 2026-03-29
  • PROOF-NEEDS.md — "dishonest by a wide margin" honesty refresh, 2026-05-18
  • No AFFIRMATION.adoc at repo root (cf. echidna / ephapax / typed-wasm)

Filed after discovering the overclaim while choosing GitHub Sponsors featured repos: proven's blurb fails the ground-truth test its own internal docs pass. Tracking issue only — fix is on the maintainer's own timeline as the (1-day-old) AFFIRMATION convention shakes out drift estate-wide.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions