Conversation
…ng 2026-05-03 P0 outstanding item from #1383 math-proofs honest assessment: drafts the peer-review outreach the maintainer 2026-05-03 named *"we are beyond cutting edge and mathecial formally verivied just not peer reviowed until you email someone"*. Maintainer customizes wording + sends; this doc is the prepared draft, not yet sent. Gates nothing. Includes: - 5-tier recipient ranking with rationale per tier: - Tier 1: DBSP paper authors (Budiu, Chajed, McSherry, Ryzhyk, Tannen) — strongest natural-interest match - Tier 2: POPL/PLDI/OOPSLA program-committee surface (Chlipala, Birkedal, Erbsen, Blazy) - Tier 3: conference Artifact Evaluation Committees - Tier 4: open-source verified-systems community (Lean / Mathlib / TLA+ / Coq-club) - Tier 5: academic-industry liaisons (MSR, INRIA, Galois) - Two email-template variants: - Tier 1 send: cites the specific paper, asks 2 calibration questions about definition-map alignment + publication target - Tier 2 send: pitches the verification-discipline pattern (per- artifact registry + drift audit) as itself potentially-novel contribution - Suggested send protocol: sequential not blast, 1-2 week gaps, threading discipline, verbatim-response-capture per substrate- or-it-didn't-happen, single nudge at 3 weeks Composes with #1383 (the A/B/C-graded artifact list), verification- registry.md (the per-artifact ground-truth), chain-rule-proof-log.md (round-by-round history), ROADMAP.md (publication target). Header carries §33 archive-header fields. Operational status: research-grade.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
Pull request overview
This PR adds a new research document that prepares external peer-review outreach for Zeta’s formal-verification work, following the readiness assessment from #1383. It fits into the research/docs layer by turning the earlier “peer-review email draft” action item into a concrete send plan and draft templates for the human maintainer to customize.
Changes:
- Adds a ranked five-tier recipient strategy for external peer-review outreach.
- Adds two outreach email templates tailored to DBSP paper authors and PL/verification committee members.
- Adds a suggested follow-up/storage protocol tying outreach back to existing research artifacts and correspondence capture.
- Replace ' + verified-IR context.' wrapped bullet with 'and verified-IR context.' (MD032 line-start + violation) - Reword 'Reaching out NOW (vs. submitting cold) is informal-feedback signal' → '... is a way to gather informal-feedback signal before committing to a specific venue' (was grammatically incomplete)
1 task
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…-correction substrate-discovery cascade (#1391) Heavy substrate-corrections cluster across #1387 + #1388 + #1390: chat-is-assertion-channel discipline + complementary-not-exclusive + hypothesis-vs-fact (live-off-the-land) + existing-prior-art (AOT- core-plus-JIT-plugins per Zeta.Bayesian) + DST-load-bearing + git- cross-check + B-0017 dashboard composition. Discipline lessons: substrate-corrections-cluster discipline (don't bundle multiple corrections in one PR; reviewer-thread-load scales linearly) + search-first-before-architectural-expansion (the git CLI/server + UI framings were already substrate).
Merged
4 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
… A1+A2 → A-with-CI) (#1394) * ci(lean-proof): add CI gate for DbspChainRule.lean type-check (closes A1+A2 → A-with-CI) Per the math-proofs honest assessment (#1383) outstanding-work matrix, the Lean proof of DBSP chain rule (Prop 3.2 + Dop_LTI_commute) was A-grade today hand-run but missing CI gating. Peer reviewers expect "runs in CI" as the line for an A-grade artifact. This PR ships `.github/workflows/lean-proof.yml`: - Path-filter: only runs on `tools/lean4/**` changes (or workflow itself). Out-of-band from gate.yml because Mathlib's lake cache is multi-GB and Lean toolchain setup is heavier than the existing build-and-test surface. - Caches `tools/lean4/.lake` keyed on lean-toolchain + lakefile.toml + lake-manifest.json (busts cleanly on either change). - Caches `~/.elan` with same key shape as gate.yml's elan cache (shared cache space). - Uses `lake exe cache get` to download Mathlib pre-built oleans from S3 — skips the multi-hour Mathlib build. - Type-checks via `lake env lean Lean4/DbspChainRule.lean`. Verified locally: `lake env lean` returns silent + exit 0 (success) on the current proof. Two corrections to #1383 captured in same PR: 1. **Semgrep is already in CI** — original B4 grading was wrong. Verified by grep: `.github/workflows/gate.yml` line ~422 has `lint (semgrep)` job running `semgrep --config .semgrep.yml --error --metrics=off`. Effective grade upgraded to A; outstanding-work item closed. This illustrates the verify-then-claim discipline. 2. **Outstanding-work matrix updated** with Status column tracking each item: "Done" (Semgrep, A4 registry rows #1393, peer-review email #1387), "In flight" (Lean CI — this PR), "open" (Stryker, B1, B2, C-grade items). Composes with verification-registry.md (rows for both A1+A2 benefit) + the verification-drift-auditor skill (every CI fire is implicit drift-check) + #1383 (the assessment doc this upgrades). Workflow safe-pattern compliant per FACTORY-HYGIENE row #43: SHA-pinned actions, contents:read permissions, concurrency group, pinned runs-on, path-filter narrows trigger. * fix(lean-proof): address review threads — add GITHUB_TOKEN env + dedupe outstanding-work row Three review threads on #1394 addressed: 1. + 3. **GITHUB_TOKEN missing**: mise's aqua: backend uses the GitHub API for release-tag lookups during install.sh; without GITHUB_TOKEN it hits the unauthenticated 60/hr rate limit and fails. Added workflow-level env: with secrets.GITHUB_TOKEN — same pattern as gate.yml. Inherits contents:read, no escalation. 2. **Outstanding-work row duplicated**: the Peer-review email draft row was inserted twice (Done + empty status). Removed the empty-status duplicate; single Done row remains.
Merged
2 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…6-05-03 EOD progress (#1402) Reflects substantive progress this session across the math-proofs honest assessment matrix. Key state changes: **P0 items — 3 of 3 closed:** - Lean lake-build CI job ✓ (#1394) - A4 registry rows ✓ (#1393) - Peer-review email draft ✓ (#1387) - Stryker B3 → partial (config-fix #1395; CI wire deferred to follow-up substantial-design) **P1 items — significant progress:** - Alloy B2 → A ✓ (#1396 — silent-no-op was the failure mode; spec-path fixed) - Semgrep B4 → A ✓ (verify-then-claim correction; was already in CI) - B1 4 deferred specs → 2 of 4 done: - DbspSpec ✓ #1397 (1M states / 11s) - CircuitRegistration ✓ #1401 (B-0180 closed; 3538 states / <1s) - SpineAsyncProtocol B-0179 still open (counterexample inv.) - SpineMergeInvariants B-0181 still open (counterexample inv.) **Sibling work tracked:** - Phase 0 substrate-discovery PoC ✓ (#1392 — 4.0 MB AOT binary on osx-arm64; cross-platform CI matrix) - 3 broken-spec backlog rows filed (#1398 → B-0179 + B-0180 + B-0181); B-0180 closed (#1401) - `.ts/.sh` parity bug in `tools/backlog/generate-index.ts` closed ✓ (#1400 — both generators byte-identical) This update is bounded substrate work documenting the actual state of the matrix; doesn't add new work, just captures completion. Future matrix re-grades happen as work-items land (per the assessment doc's audit-trail discipline). Composes with #1383 (the original assessment) + every PR referenced above. §33 archive-header lint passes.
2 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…ster + cache-clobber discipline encoded (#1408) Substantial multi-tick session shard. 18 PRs touched (#1383 + #1387 + #1392-#1407 inclusive); 14 merged + 4 in-flight as of shard time. **Math-proofs assessment progress** (#1383 outstanding-work matrix): - A1+A2 → A-with-CI ✓ (#1394 Lean lake-build workflow) - A4 registry rows ✓ (#1393) - B1 → 2 of 4 deferred specs in CI ✓ (#1397 DbspSpec + #1401 CircuitRegistration B-0180 closed) - B2 Alloy → A ✓ (#1396 silent-no-op spec-path fix) - B4 Semgrep → A ✓ (correction) - Peer-review email template ✓ (#1387) - Phase 0 substrate-discovery PoC ✓ (#1392) - Stryker config-fix ✓ (#1395; CI wire deferred) - 3 broken-spec backlog rows filed ✓ (#1398) **Cache-clobber silent-bug class discovered + fully encoded:** B-0180 fix passing locally + failing CI → verify-then-claim identified gate.yml + low-memory.yml caching whole tools/tla and tools/alloy directories. Fix cluster: #1403 (gate.yml) + #1404 (low-memory.yml + audit-ci-cache-paths.ts) + #1406 (CI lint gate) + #1407 (memory file + bug-locus disambiguation per Aaron's 'real github bug?' question — answer: usage-bug, not tool-bug). **Other substrate work:** #1399 BACKLOG.md regen, #1400 .ts/.sh parity bug, #1402 assessment matrix doc update, #1405 B-0182 backlog row (Linux-only formal verification — orthogonal-axes split per Aaron 2026-05-03). **Discipline lessons captured:** chat-is-assertion-channel, substrate-corrections-cluster, search-first-before-architectural- expansion, verify-then-claim CI fidelity, documentation-is- current-state-not-history. Carved sentence: 'When a lucky catch surfaces a class of bug, build the structural fix that eliminates the luck — audit + lint gate + carved-sentence rule + memory file.'
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
P0 outstanding item from #1383 math-proofs honest assessment: drafts the peer-review outreach the maintainer 2026-05-03 named.
Maintainer customizes wording + sends. This doc is the prepared draft. Gates nothing.
Includes
Architect call within authority
Maintainer 2026-05-03 surfaced the ask-permission-within-authority failure mode. The right response: draft the template within authority; you customize + send; storage for replies preserved at
docs/research/peer-review-correspondence/per substrate-or-it-didn't-happen.Test plan
🤖 Generated with Claude Code