[wildcard] Make hy-check an untrusted proof producer: permission certificates for actual Go

The idea, in a paragraph

For an opt-in certified subset, make neither hy-check nor hy-emit trusted for the emitted artifact's race-freedom claim. They produce Go plus a candidate permission derivation; an independent kernel checks that derivation against the actual typed Go CFG, including allocations, aliases, reads/writes and spawn/send transfers. A frontend ACCEPT or a certificate merely asserting ‘sendable’ is not evidence. The research question is whether explicit proof checking can remove inference/search from the trusted safety core without becoming another full checker.

Which assumption it breaks

Challenge trusting hy-check's implementation for the certified artifact's safety. At inspected main 1f0ff978f4deff78c77bca96db0e3e46f32de71b, stmt.rs:39–69 intentionally erases move markers and emits ordinary Go sends/goroutines. That is not a bug report. Could the resulting artifact instead carry independently checked safety evidence even when inference is wrong?

Why this is a breakthrough, not an increment

W-013/#345 explicitly keeps hy-check trusted and verifies checked-IR-to-Go preservation. Here the checker is also an untrusted proof producer; the target is a direct safety property of actual Go.
W-004/#174 relies on phantom witnesses and cmd/compile. This kernel would check permission/alias derivations for supported storage and reject unsupported captures; ordinary Go type-checking alone cannot certify it.
W-023/#565 uses toolchain/test oracles. Finitely many successful executions are not a proof derivation.

Proof-carrying code is established work, not a claimed invention here. The bounded tracker searches did not identify this same trust-boundary change; they are not an exhaustive novelty proof. If maintainers group it with an existing family, shared evaluation or decline is preferable to duplicate work.

How we would know it works (or doesn't)

Initial boundary: a closed program with scalar inputs and internally allocated storage. Support scalars, slices of scalars with explicit backing roots, static callees, branches, and one-way spawn/send ownership transfer. Borrowed mutable entry inputs, mutable globals, loops, defer/panic/recover, closures, maps, FFI, managed code, unsafe, reflection and unresolved dispatch initially receive no certificate. Calls require a checked callee derivation in the same closed artifact.

Obligation: cover every actual CFG edge and memory operation. Reference copies retain their backing-root identity; only a checked allocation rule creates freshness. Write permission cannot be duplicated among concurrently live tasks. Check join assertions rather than trust them. Bind the proof to the full Go input set actually compiled, build tags/platform/toolchain configuration, checked callee derivations, semantics and kernel version.

Proposed falsifier/control	Required outcome
Supported spawn/send with actual reads/writes and uniquely transferred storage	Accept
Surviving-alias writes after transfer; overlapping concurrent slice writes	Reject
Forged freshness/sendable labels, omitted CFG edges, unsafe type-correct output mutations	Reject independently of hy-check
Unsupported constructs, changed artifact, incomplete derivation	No certificate
Race-free but functionally wrong output	May pass safety; must still fail the separate behaviour gate

An illustrative in-subset negative case (not run) is x := make([]int, 2); alias := x[:1]; go write(x); alias[0] = 1, with a statically known write that mutates the overlapping element. The kernel must reject this even with forged permission annotations; rejection must not merely rely on an unsupported closure or foreign feature.

Before prototyping, publish the exact case/mutation inventory and trust ledger. Proposed budget: at most 2,000 non-generated semantic-rule LOC, locally checked rule/dataflow replay only (no global invariant or proof search), and no new SMT-solver trust. List Go frontend dependencies separately and compare both designs on the same admitted features; shrinking the language is not itself a trust reduction.

Reject or narrow the thesis if meaningful positive cases cannot be certified, unsafe variants pass, permissions still depend on trusted hy-check labels, the kernel copies the existing search engine, or added dependencies defeat the trust reduction.

Cost honesty (optional but powerful)

A restricted-Go semantics, proof format, producer and independent verifier may cost more than they save. Go parsing/type resolution, kernel rules, and the Go compiler/runtime remain trust assumptions. A toy safe subset is not a convincing success.

This certifies neither source equivalence nor business-result correctness, foreign code, or arbitrary Go. Those separate obligations remain. Existing semantics and the native backend must not silently weaken.

If selected, M1 is this written hypothesis and falsification plan; M2 publishes an accept/narrow/reject learning and trust/scope ledger, with illustrative arguments distinguished from experimental evidence. Any execution gets a separately preregistered scope. No prototype, tests, benchmark or formal safety result has been produced.

One wildcard winner is selected per cycle. Submission, acknowledgement or a ledger slot is not an award or receivable.

Sources reviewed at the inspected commit: BOUNTY.md, MOONSHOT.md, GUARANTEES.md, README, AGENTS, the wildcard template, and the linked related proposals.

Track terms

I understand no prototype is required and failure-with-knowledge is a valid, paid outcome
I understand all outcomes (including declines and failures) are published in MOONSHOT.md

/attempt

/attempt #2176

Submitted complete independent verification kernel and executable falsifier suite in PR #2402:

Native Go kernel (<200 LOC, zero SMT/global search) enforcing typed CFG coverage and memory operation accounting.
Python deterministic replay engine passing all 5 falsifiers (F-01 through F-05) covering unique transfer, surviving aliases, concurrent slice overlap, forged bounds, and omitted CFG edges.

Pull Request: #2402
Settlement Wallet (Solana / USDC): BU5zBur46YjnCaY34XGBTJ8KSAG9EExjpZA58wDo7wAx

feat(spikes): add W-025 untrusted proof producer kernel & falsifier s…

Adding one piece of evidence to this proposal, because I hit the exact failure mode it names and it is the strongest argument I can make for the trust-boundary change.

Claim in the proposal: "A frontend ACCEPT or a certificate merely asserting 'sendable' is not evidence."

I can show what that costs in practice, today. On main, with hyb built locally (rustc 1.99.1, HYB_PINNED_RUST=1.99.1), the A5 Go-escape check-site HYB-E3013 accepts four shapes of the same unsound program. All four are OK (0 diagnostics):

// A. via a local variable
    hits := 0
    h := fn(w, r) { hits = hits + 1 }
    mux.handle("/x", http.handler(h))

// B. via a slice element
    handlers := [fn(w, r) { hits = hits + 1 }]
    mux.handle("/x", http.handler(handlers[0]))

// C. via a map value
    m := map[string]fn(w http.response_writer, r *http.request){"x": fn(w, r) { hits = hits + 1 }}
    mux.handle("/x", http.handler(m["x"]))

// D. declared, assigned later
    var h fn(w http.response_writer, r *http.request)
    h = fn(w, r) { hits = hits + 1 }
    mux.handle("/x", http.handler(h))

The identical program with the closure inline is rejected. The root cause is that check_escape_site matches Expr::FnLit in the argument list and nothing else — Expr::Ident, Expr::Index and assignment-after-declaration never reach closure_writes_captured at all.

Why this is an argument for the proposal and not just a bug report: those four are not four bugs, they are one bug — a syntactic pattern standing in for a semantic property. The property "this closure captures a mutable binding it writes" does not change when you move the closure through a variable, a slice, a map, or a later assignment. The checker's certificate would have been identical in all five cases, and the certificate would have been wrong in four of them. That is exactly the class of failure a derivation checked against the actual typed Go CFG cannot make: the derivation has to name the capture and the path by which the closure reaches the foreign call, and none of those four shapes can produce such a derivation.

So the proposal's "reject unsupported captures" clause is not a corner case — it is the whole point. Today, unsupported captures are not rejected; they are silently treated as absent. If the kernel refuses to certify what it cannot derive, all four shapes become REJECT-not-CERTIFIED rather than ACCEPT, which is the correct outcome and does not require any new inference.

One soft spot in the proposal as written. "Whether explicit proof checking can remove inference/search from the trusted safety core without becoming another full checker" is the right question, but the milestone list makes the kernel's first version depend on "slices of scalars with explicit backing roots" and "one-way spawn/send ownership transfer" and static callees. I would cut that to the smallest artifact that still falsifies the idea: scalars and internal allocations only, no transfer, and check one property — that no closure reachable by any path from a foreign call writes a captured mutable binding. That single property, checked against the real Go, would have caught A–D. If the kernel cannot express that, the larger surface is not worth attempting first.

Note on prior work. The four shapes above are already reported upstream of me: #2418 item 2 covers A; B, C and D I commented on #2418 as possibly-uncovered sub-cases. I am not claiming those as new findings — I am using them as the evidence this proposal needs, since the proposal's whole argument is that frontend ACCEPTs are not evidence.

Disclosure: I am the author of #2588 and I commented on #1962. I built hyb from main and checked 15 check-site surfaces; four came out clean (option[map], channel send of a closure, any-wrapped closure, task-closure), which is context for why I trust the sendability core and distrust only the syntactic match. I have not read hy-emit (137 KB in stmt.rs), so I cannot judge how hard the CFG extraction is — that is the proposal's real cost and I am not pretending otherwise.

feat(spikes): add W-025 untrusted proof producer kernel & falsifier s…

@mak777uh

@mak777uh Thanks for the examples and prior-work attribution; I have not independently rerun them. The callback/closure probe would be a separate diagnostic, not a strict reduction of the posted subset: the original excludes closures and FFI while admitting scalar-slice transfer. I would retain that original same-feature comparison and preregister the callback property separately if pursued.

@theheiszt Thanks for #2402. From a static read of 9a2c4a3, VerifyProof receives actualCFG and actualOps from its caller. The remaining obligation is binding those lists to the complete actual typed Go artifact with an explicit extraction trust boundary; hand-authored graph fixtures alone do not establish that binding.

For clarity, #2252 and #2402 are third-party contributions, not my implementations or test reports. #2252 is currently unmerged; its proposed ledger entry and settlement details are not part of my written proposal and do not by themselves establish acceptance or an award.

My submission remains an unimplemented hypothesis with separate safety and behaviour gates, rather than experimental validation.

Navigation Menu

Repository navigation

[wildcard] Make hy-check an untrusted proof producer: permission certificates for actual Go #2176

The idea, in a paragraph

Which assumption it breaks

Why this is a breakthrough, not an increment

How we would know it works (or doesn't)

Cost honesty (optional but powerful)

Track terms

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

[wildcard] Make hy-check an untrusted proof producer: permission certificates for actual Go #2176

Description

The idea, in a paragraph

Which assumption it breaks

Why this is a breakthrough, not an increment

How we would know it works (or doesn't)

Cost honesty (optional but powerful)

Track terms

Activity

t3ratech commented on Oct 29, 2026

theheiszt commented on Oct 31, 2026

mak777uh commented on Oct 31, 2026

2011722761 commented on Nov 2, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions