Hacks Phil would have stopped
Four well-known losses. Each one comes down to a simple kind of mistake. Below, the same mistake is written in Phil and run in your browser, so you can watch it get refused, then see what the working version looks like.
These are not the original contracts. They are the shape of each mistake, small enough to read. The claim is that Phil refuses this kind of error, not that it would have rescued that exact project.
What Phil would not have stopped
Most of the largest recent losses were not coding mistakes of this kind. A language cannot help with these:
The programs here run in this project's experimental simulator, which is our own reading of Phil. Real Phil is designed to prove these properties before a program runs; the simulator finds them by running it.