bincode · 2024
One maintainer rewrote git history while migrating off GitHub. The community asked questions. The questions became doxxing. The project shut down permanently. There is no 1.3.4.
r/rust thread →Veridict is a merge gate for synthesized code. Three formal proofs verify the PR. One ZK signature authorizes it. Zero identities revealed.
Vibe-coded code shouldn't merge on vibes.
It should merge on proof.
Four incidents. One pattern. The same architectural hole shows up over and over again, in projects that have nothing else in common.
One maintainer rewrote git history while migrating off GitHub. The community asked questions. The questions became doxxing. The project shut down permanently. There is no 1.3.4.
r/rust thread →"Jia Tan" earned maintainer status over two years, then shipped a backdoor that nearly compromised sshd on every major Linux distro. Caught by accident, weeks before stable release.
post-mortem →"My job is increasingly fact-checking the AI," wrote Daniel Stenberg. Open-source maintainers are drowning in plausible AI PRs that pass surface checks and fail on invariants.
Stenberg's blog →Karpathy coined it. The hackathon brief quoted the discomfort: "we have no way of knowing if what we're vibecoding does what we think it does." The practice went mainstream anyway.
hackathon brief →No checklists. No vibes. Each PR walks the same path from English spec to anonymous merge approval, and the issuer refuses to sign if any of the three formal layers fails.
Claude turns your spec into an implementation, a pytest suite, and a Z3 invariant file. The bot opens the PR for you.
mypy checks types. pytest checks behaviour. Z3 checks invariants symbolically. Any failure → no credential.
A Longfellow proof replaces your identity with a stable per-PR pseudonym. N proofs land → merge button unlocks.
The issuer runs mypy, pytest, and Z3 against the PR before minting a credential. Failures break the chain. There is no "force-approve."
$ veridict verify pull/11→ fetching files@a8c4f2…✓ mypy 0 errors✓ pytest 14 passed in 0.34s✓ z3 all invariants UNSAT for negation credential issued → valid 10mbound to a8c4f2 · role=maintainer
Every approval is a 360 KB Longfellow proof that you hold a credential. The PR author, the bot, and the audit trail see a pseudonym, not a face. The proof, not the person, speaks.
Anonymity is toward the verifier: CI, the PR author, and the audit trail. The issuer still sees your OAuth identity at credential time. We say so out loud.
A weekend prototype is allowed limits, as long as it names them. Here are ours.
A reviewer with two sessions can sign two approvals on one PR. They look like two pseudonyms. Production fix: derive a blinded ID inside the ZK circuit.
For demo speed. A real deployment would generate the device key in the browser so the issuer never sees it.
mypy + pytest + Z3 only run on .py files. Non-Python
PRs pass through unverified. Dafny, Rust, Lean are obvious
next stops.
Every anonymous approval posts as @anonymous-review-bot.
Pseudonyms + identicons inside the comment do the
distinguishing.
Try Veridict on a real PR. The demo repo is wired up with branch protection, and your anonymous approval flips the gate.
Sign in with GitHub