# Proof-Carrying-Code

- **Event:** [Meta Global AI Developer Hackathon](https://cerebralvalley.ai/e/meta-ai-developer-hackathon)
- **When:** Oct 26, 12:00 PM – Nov 4, 9:00 PM (EST)
- **Where:** Online
- **Team:** [Benedikt Hoster](https://cerebralvalley.ai/u/behos), [Nikita Buls](https://cerebralvalley.ai/u/nktbls), [Mick Soete](https://cerebralvalley.ai/u/MickSoe)
- **GitHub:** https://github.com/hosbe1/Proof-Carrying-Code-Meta-AI-Hackathon-2026
- **Demo video:** https://youtu.be/RtD7O5u4MoU
- **Gallery:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery
- **Page:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2689

Your AI wrote the code. Who proves it's right?

Proof-Carrying Code checks Python functions with formal proofs. Every function ends with one of two things: a proof anyone can re-check, or the exact input that breaks it, as a failing test you can run. Meta's models do the reasoning. Dafny, a proof checker, decides what counts, so a model can't talk its way past it.

What you get per function
- A proof file anyone can verify with dafny verify
- Or a counterexample: a concrete input that really breaks the spec, as a ready-to-run pytest
- Or an honest "couldn't check, and here's why"

How it works
- It reads what the function is supposed to do and writes a spec. Those steps never see the function body, so the spec can't just copy the code.
- It translates the function to Dafny and tries to prove it, with escalating Meta models.
- It runs as a GitHub Action on every pull request and posts the result as a comment.

Meta's models in the pipeline: Spark, Wonder, and Glimmer, which we fine-tuned ourselves. We trained it with rejection sampling, where the Dafny checker was the only reward and no human labels were used. On 569 held-out tasks, pass rate went from 7.6% to 44.8% (four tries per task).

## More from Meta Global AI Developer Hackathon

- [ScreenGuard](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2686)
- [Spekios](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2687)
- [Antinoise](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2688)
- [Glimmer System One](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2690)
- [zaxyar](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2691)
- [PodAI](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2692)

---

Markdown version of https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/2689. Site index for agents: https://cerebralvalley.ai/llms.txt · full text: https://cerebralvalley.ai/llms-full.txt