# ProofForge

- **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:** [David William Silva](https://cerebralvalley.ai/u/davidwsilva)
- **GitHub:** https://github.com/davidwilliam/proof_forge
- **Demo video:** https://youtu.be/j3SM-y2o-XQ
- **Gallery:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery
- **Page:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1247

ProofForge turns Meta's Muse models into provers of financial code.

AI agents now write and repair code that moves money, and tests only cover the inputs someone thought of. ProofForge states what a component must guarantee as locked Lean 4 requirements. It refutes code that breaks one with a counterexample the Lean kernel checks, and accepts a fix only when six independent kernels check its proof, the axiom audit passes and the executable built from the same source passes 2,001 property cases. Every verdict is a Passport, bound by hash to the specification, the source and the executable, that anyone can re-run. No proof, no merge.

ProofForge plugs into Muse Code, Meta's coding agent, as an MCP server and a skill: Muse Code gets the judge, kernel-checked counterexamples, a Lean session, a library of 2,051 finance theorems and the Passport, inside the coding loop.

Measured, preregistered, same model and same caps ($10 and 4 hours per run), Muse Code on its own against Muse Code with ProofForge:
- OpenZeppelin Math.sqrt behind the Aerodrome first deposit, repaired from a seeded six-step variant (OpenZeppelin's released code is correct) and proved exact for every 256-bit input: 10 of 10 with ProofForge at $1.99 per verified run, 0 of 10 on its own after $95.45 (one-sided Fisher exact p = 5.4e-6).
- Compound Proposal 62 (COMP reward distribution, at worst $80M): 0 of 10 on its own after $91.74, 8 of 10 with ProofForge at $6.97 per verified run (one-sided Fisher exact p = 0.00036); 0 of 30 on its own across three experiments. No run of any method had verified this task before ProofForge.
- Vyper sqrt (CVE-2025-26622): 10 of 15 on its own, 14 of 15 with ProofForge, 2.1x cheaper per verified run.
- Balancer V2 (more than $120M drained from Balancer and its forks): 2 of 5 on its own at $20.02 per verified repair, 3 of 3 with ProofForge (Muse Wonder plans, Muse Spark proves) at $3.06.
- Muse Spark Open, Meta's open-weight model, preregistered: 22 of 30 test tasks on its own, 24 of 30 with ProofForge, and every executable with ProofForge passed the property tests (30 of 30). Across both experiments, 48 of 60 against 43.
- Seeded bad repairs: ordinary checking accepted 233 of 247, ProofForge 0, with 0 of 239 correct repairs rejected.

Six real failures with more than $1 billion in reported losses (Cetus, Balancer, Euler, Knight Capital, Hundred, Compound) are each refuted on their vulnerable code by a kernel-checked counterexample, and five of the ports are run against the real code: Balancer, Hundred and Compound on chain forks, Cetus and Euler at their pinned source commits (Knight Capital's code is not public). 569 measured runs, 268 comparisons, every one kept in a public ledger.

Live: https://proofforge.dev (the Balancer exploit replay is at /app, the comparisons at /frontier).

## More from Meta Global AI Developer Hackathon

- [Atelier Busco](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1244)
- [ReturnWitness](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1245)
- [Jonathan_Stokes](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1246)
- [Team M.E.G.A](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1248)
- [DataSec Chronicles](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1249)
- [Courio](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/1250)

---

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