The usable formal methods hackathon. Build a piece of real-world production software, and formally verify it.
A 25-second loop. Click it to pause, or open it on its own page to jump between scenes.
Formal methods have officially entered the zeitgeist. But are these techniques actually ready for prime time?
We know FM can be brought to bear on stodgy academic software: basically mathematical in nature, not reliant on external dependencies, and lacking a GUI, a database, or third-party APIs. But could it be brought to bear on Microsoft Word, or Flappy Bird, or Claude Code? Is FM ready for truly mainstream adoption? Could the next hot YC company build its product to be formally verified from the very start, without needing to first complete a PhD at Carnegie Mellon?
To answer these questions, we're running a hackathon. Teams pick a piece of software people would actually use, build it, and prove it correct. Work alone, bring a team, or find one in the room.
Competitors are people with little or no formal methods experience; experts are people with a lot of it.
Zero to not a lot of FM experience. Build a piece of real-world production software and formally verify it. Solo, with a team you bring, or with people you meet on the day.
Significant FM experience. A year or more of full-time work with at least one FM tool, or close to it. Walk around the room and unstick competitors when they get stuck.
Provide prizes, swag, food, compute, tokens, and other things that make a weekend go better.
We are targeting a ratio of roughly five competitors to one expert, so there is always someone nearby who has seen your error before.
If you're interested in participating, in any capacity, fill out the form. It asks about your availability, how you'd like to take part, your FM background, a few prior projects you're proud of, and whether there's something specific you want to build. No project idea is needed to sign up.
Questions? Email quinn@for-all.dev.
Vibecheck is made possible by these organizations. Thank you.
Want to sponsor too? Sign up as a sponsor, or email quinn@for-all.dev.