Proof-Carrying-Code

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).