Summary
leanaudit (trailofbits/leanaudit) is the project-side soundness checker that audits axioms, sorries, classical/constructive split, and dependency cycles per Lean module. We initially wired it as a CI job in PR #3 but had to drop it because:
trailofbits/leanaudit repository visibility is INTERNAL.- The default
GITHUB_TOKEN in our validation-harness.yml workflow only has access to scroll-fv itself, not other org-internal repos.
uv tool install git+https://github.com/trailofbits/leanaudit.git therefore fails with fatal: could not read Username for 'https://github.com' — git tries to prompt for credentials and exits non-zero.
What's needed
A fine-grained PAT (or GitHub App installation token) with read-only access to trailofbits/leanaudit, stored as repo secret LEANAUDIT_TOKEN on trailofbits/scroll-fv.
Step-by-step
-
Create the token at https://github.com/settings/personal-access-tokens/new
- Token name: e.g.
scroll-fv → leanaudit (read)
- Resource owner:
trailofbits
- Repository access → Only select repositories →
trailofbits/leanaudit
- Repository permissions → Contents → Read-only
- Generate, copy the token.
- Note: trailofbits org may require admin approval for fine-grained PATs (token shows as 'Pending' until approved).
-
Add as repo secret at https://github.com/trailofbits/scroll-fv/settings/secrets/actions
- New repository secret
- Name: `LEANAUDIT_TOKEN` (exact)
- Value: paste the token
-
Re-add the job in `.github/workflows/validation-harness.yml`. The previous shape (commit `57806a2` in this repo's git history) is the right starting point — it already gates on `secrets.LEANAUDIT_TOKEN` and skips with `::warning::` when absent.
Acceptance criteria
Summary
leanaudit(trailofbits/leanaudit) is the project-side soundness checker that audits axioms, sorries, classical/constructive split, and dependency cycles per Lean module. We initially wired it as a CI job in PR #3 but had to drop it because:trailofbits/leanauditrepository visibility is INTERNAL.GITHUB_TOKENin ourvalidation-harness.ymlworkflow only has access to scroll-fv itself, not other org-internal repos.uv tool install git+https://github.com/trailofbits/leanaudit.gittherefore fails withfatal: could not read Username for 'https://github.com'— git tries to prompt for credentials and exits non-zero.What's needed
A fine-grained PAT (or GitHub App installation token) with read-only access to
trailofbits/leanaudit, stored as repo secretLEANAUDIT_TOKENontrailofbits/scroll-fv.Step-by-step
Create the token at https://github.com/settings/personal-access-tokens/new
scroll-fv → leanaudit (read)trailofbitstrailofbits/leanauditAdd as repo secret at https://github.com/trailofbits/scroll-fv/settings/secrets/actions
Re-add the job in `.github/workflows/validation-harness.yml`. The previous shape (commit `57806a2` in this repo's git history) is the right starting point — it already gates on `secrets.LEANAUDIT_TOKEN` and skips with `::warning::` when absent.
Acceptance criteria