Machine-Checked Devcon Week（Invisible Garden 线上黑客松，用 Lean 4 实现以太坊网络层并写机器可验证证明）
这场已截止报名 · 还在报名的同类比赛
- Dabao Open Hardware Hackathon（开源芯片开发板黑客松，最高 $5,000）$5k · 截止 12-15
- Agents on Open Rails 黑客松（Celo，做能在主网真实收付款的 AI Agent，线上，5,000 美元）$5k · 截止 11-09
- Total Recall 黑客松（Walrus × Tatum，给应用和 Agent 加上链上长期记忆，线上，4,500 美元）$4.5k · 截止 11-10
- MozFest Developers Wilding: Online（Mozilla 线上黑客松，用 Mozilla.ai 开源平台 Otari 把搁置的项目做完）$1.2k · 截止 11-11
- NEAR HACKATHON 2026（NEAR 基金会，AI 智能体 × 链上支付，$25 万）$250k · 截止 11-14
- Code for a Billion 黑客松 2026（印度公益 Agentic AI）截止 11-15
- 状态
- 截止
- 2026-11-01
- 面向
- 不限（不限水平，要会写代码、对 Lean 或形式化验证感兴趣；需申请审核，名额不到 10 人）
- 难度
- 硬核
- 奖金
- $1k · 奖池 1,000 美元（Invisible Garden、EthPadThai 各 500），更多赞助确认中；实际参与少于 7 人时奖池可能缩减
- 人数
- —
- 形式
- 线上 · 海外
- 地图
- 孟买（线上，按主办方所在地估测）
更多来源主办方 X 帖 ↗
更多同类线上黑客松Web3 区块链黑客松开源黑客松2026年11月黑客松
原文
一句话简介：以太坊开发者游学项目 Invisible Garden 在 Devcon 周办的线上黑客松，用 Lean 4 实现以太坊网络层的模块，并为自己写的代码写出由 Lean 内核检查的证明。
看点：任务都在 leanp2p 仓库的 issue 里，依赖的 issue 合并后才能认领；评论 claim 后 8 小时内要开 PR，否则释放；组织者 12 小时内审核；得分 = 代码质量 × 有证明覆盖的比例；免费参加，但需申请，录取不到 10 人，在 Discord 公布；要交最长 10 分钟的讲解视频，否则不评
奖金：奖池 1,000 美元，更多赞助确认中
截止日期：11 月 1 日申请截止（11 月 7 日 23:59 UTC 代码截止，即北京时间 11 月 8 日 7:59；11 月 15 日交视频）
活动日期：2026年11月2日—7日（全球线上），11月30日前公布结果
信息整理自主办方页面和公开帖子，报名前请以官网为准。