Machine-Checked Devcon Week
An online hackathon during Devcon week: learn Lean 4, formal verification, and Ethereum networking by building.
Community partners
What it is
Learn by shipping real protocol work
Machine-Checked Devcon Week is an online hackathon, run during Devcon week, 2 to 7 November 2026. You pick real protocol tasks from a public repo and learn by shipping code and proofs.
Participation is curated. You apply, the organisers review, and acceptances are announced in the event channel on the Invisible Garden Discord.
The cohort stays under ten contributors, small on purpose, so your work gets real attention.
Participation is free, and the Invisible Garden community rules apply all week.
The work
Implementation and proofs together
You implement pieces of Ethereum's networking layer in Lean 4 and prove properties of what you build. Every proof is checked by Lean's kernel, and implementation and proofs live together in one codebase.
The tasks live in the leanp2p repo on GitHub.
Who should apply
Any level counts
The week is for people at or around Devcon: the Lean curious, Ethereum protocol developers, and the Invisible Garden and EthPadThai communities.
You should apply if you are curious about Lean or formal methods and comfortable writing code. Any level counts. What matters is motivation and drive.
The form asks about your experience and why you want in. It is short.
The rules
How the week works
All work lives in the issues of the leanp2p repo. Issues depend on each other, and closed means merged: a dependency still in review keeps the next issue closed to claims.
- Pick an issue. You can claim an issue once every issue it depends on is closed, and closed means merged.
- Claim it. Comment "claim" and an organiser assigns it to you. One issue at a time.
- Open a PR within 8 hours. The clock starts at assignment, drafts count. Link the issue in the PR.
- Miss the window, lose the claim. No PR after 8 hours and the issue is unassigned. Anyone can claim it again.
- Review and merge. Organisers review within 12 hours. When your PR merges, the issue closes and the issues depending on it open for claims.
- Repeat. Claim, build, prove, submit, all week.
These are the rules in full. Until the leanp2p repo carries its own RULES.md, this page is canonical.
Everything runs on the clock in UTC. Organisers and mentors answer questions in the event channel all week, and acceptances are announced there.
Dates
Deadlines and judging
- Code closes 7 November 2026, 23:59 UTC. Every PR you want judged must be open by then, with CI green. Merges can land later.
- Video by 15 November 2026, 23:59 UTC. Up to 10 minutes, you explaining your contributions, link in the event channel. Unlisted is fine. Without a video, the work is not judged.
- Judging by 20 November, results by 30 November.
How entries are scored
Submissions are scored on two axes, code quality and how much of the work carries machine-checked proofs, and the final score multiplies the two. Well engineered code earns its value together with proofs.
Prize eligibility*
Prizes recognise meaningful contributions. The judges assess your whole body of merged work from the week, and they have the final say on what counts. The baseline:
- Your work closes at least one claimed issue, with the PR opened before code close and merged.
- The contribution is real implementation work or real proof work. Mechanical changes, typo fixes, formatting, dependency bumps, and trivial refactors do not count by themselves.
- You can explain and defend your work in the video, including your reasoning and your proofs. A contribution you cannot defend in the video does not count for prizes.
- All counted work falls inside the event window, 2 to 7 November.
If a participant's overall contributions stay at a basic level, the judges may rule them out of prize consideration. The week is still worth it: the work is public, the learning is yours, and every merged PR is yours to show.
* With fewer than 7 active participants, the prize pool can be reduced.
Prizes
$1,000 and growing
Invisible Garden and EthPadThai have each confirmed $500. More contributors are being confirmed.
The pool is a thank you, not the reason to join. The full rules, including eligibility, are on this page.
Who runs it
Organisers and partners
Invisible Garden organises the week. Invisible Garden is a traveling academy for Ethereum developers, with editions in Chiang Mai in 2024 and Buenos Aires in 2025.
EthPadThai, 4Seas, EthTAO and Eth Cinco de Mayo are the community partners of the week.
The week is part of Road to Devcon, supported by the Devcon organisation.
The tasks live in the Etheorem project's leanp2p repo.
Apply by 1 November
Applications close 1 November 2026. The week runs 2 to 7 November, online, with a cohort under ten.