Independent audit — status, scope, and how to do one

Plainly: this repository has NOT been independently audited. It is self-verified and fully reproducible, which is not the same as a third-party audit. This file says exactly what that means, what an auditor should check, and how to reproduce everything.

1. Status (honest, up front)

Question	Answer
Independently audited by a third party?	❌ No
Peer-reviewed formally (academic/industry)?	❌ No
Reproducible by anyone (sources + code)?	✅ Yes
Automated tests of the tool logic?	✅ Yes — `examples/self-test.mjs` + CI
Executable model + property check?	✅ Yes — `examples/model-check.mjs` (offline, 2000 seeds)
Exhaustive (bounded) verification?	✅ Yes — `examples/exhaustive-check.mjs` (all 1452 histories in a finite domain)
Does passing tests prove the whole mathematical claim?	❌ No — tests check the tool, not the proof

⚠️ Do not read “tests pass” as “audited.” Automated checks verify the behaviour of one script against one transaction. An audit is a human review of the claims, the proof, and the code together.

2. What “independent audit” would mean here

An auditor is a third party (not the author) who, with adversarial intent, checks that:

The claim is stated precisely — before checking anything, is the claim even well-posed? (It is: “a native Pi payment carries no observable per-unit mining origin on the Pi Mainnet ledger.”)
The proof is sound — every step in SCOPE.md §7 / PROOF.md follows, with no hidden assumption.
The sources say what is attributed to them — every quote in SOURCES.md matches the official document (docs.minepi.com, the MiCA whitepaper, the Platform API docs).
The code does what it claims — read-only, no hidden calls, and its output matches a manually computed result.
The scope is respected — that claims A / B / C (below) are not conflated, and that nothing beyond the stated claim is implied.

Only (1)–(5) together, done by someone other than the author, would be an audit. None of them is claimed as done by a third party.

3. The three claims (so an auditor knows what to attack)

#	Claim	Evidence in this repo	Audited?
A	Protocol fungibility — no observable per-unit mining origin	`SCOPE.md` §7 (formal), `PROOF.md`	❌ not by a third party
B	A specific transfer is a real native Pi payment on Mainnet	`examples/verify-deposit.mjs` + `self-test.mjs`	✅ logic self-tested; ❌ not third-party
C	A venue’s total internal balance is fully backed on-chain	—	❌ not claimed (off-chain)

See FAQ-EXCHANGE-DEPOSIT-VERIFY.md for the full separation.

4. Reproduce everything yourself (≈ 5 minutes)

Requires only Node 18+ (no npm, no dependencies) and network access.

git clone https://github.com/aybvip/pi-fungibility
cd pi-fungibility

node examples/self-test.mjs          # 26 offline checks (validators + evaluate + transport failures) + 3 online end-to-end checks
node examples/model-check.mjs        # offline ledger model + property check (2000 seeds, deterministic)
node examples/exhaustive-check.mjs   # offline EXHAUSTIVE bounded check (all 1452 histories)
node examples/coin-id-check.mjs      # no per-micro-π identifier on the ledger
node examples/provenance-check.mjs   # a live account with many inbound payments, one scalar balance
node examples/mixing-check.mjs       # mined + bought -> one balance -> origin-less payment

Then read, against the code, the claims in SCOPE.md / PROOF.md. Everything the repo asserts about the protocol is either a quoted official source or a plain node script you just ran.

🔧 The scripts are intentionally tiny and dependency-free so they can be read line by line — see SECURITY.md for the read-only guarantee (no wallet, no keys, no signing).

5. Known limitations (the auditor’s checklist)

Attack the falsifiers first. The claim is falsifiable and the falsifiers are listed: a per-unit field, a protocol allocation rule, a non-scalar balance, or one counterexample transaction — any one kills it. See FALSIFICATION.md. Two are attempted by examples/falsify-try.mjs.
Formal proof is not machine-checked in a proof assistant. §7 is a written argument, not a Lean/Coq artifact. We provide an executable model + property check (examples/model-check.mjs, 2000 seeds) and an exhaustive bounded check (examples/exhaustive-check.mjs, all 1452 histories in a finite domain) — both offline. Strong, but bounded; still not the same as a verified formalisation.
Sources are as of their publication date. If Pi Network changes the protocol or its docs change, re-verify (see SOURCES.md for dates/links).
The live examples depend on the network. They query https://api.mainnet.minepi.com; a specific account/tx could change over time. The sample outputs are committed as snapshots (examples/*-output.txt) — the method, not the numbers, is the point.
“Native” ≠ “backed”. See Claim C — deliberately out of scope.
No security guarantee. This is analysis, not financial or security advice (DISCLAIMER.md).

6. Find a problem? Report it

Errors are welcome — that is the point of a public, reproducible repo.

Open an issue with: the claim at stake (A/B/C), the source or command, and the observed vs expected.
If it is about the code’s behaviour, include the exact command line and full output.
If a quote is mis-attributed, link the official source so it can be corrected.

The standard we hold ourselves to: audit, don’t trust — including this repository itself. Until a third party does that, the correct label is “self-verified, reproducible, not independently audited.”

Sources

SCOPE.md §3.4 (no independent audit claimed) · SECURITY.md · PROOF.md
SOURCES.md · DISCLAIMER.md