Does It Actually Hold?
Feynman's "apply it" test, made concrete. A passing test samples a handful of inputs and reports back. A proof covers every input the type system allows — including the ones you didn't think of. Toggle a bug into the verified function below and watch the difference: the test suite stays green, but the proof flips from ✓ proven to ✗ not proven the instant the guarantee is broken.
How This Works
When you click Verify with Dafny, your source is sent to a real Dafny verifier running on a HuggingFace Space — not a pre-computed verdict, not an in-browser simulation. The verifier runs the full proof obligation and returns either a verified result or the first counterexample it finds. What you see is what Dafny actually said.
The Space may take 30–60 seconds to wake up on the first request (HuggingFace cold start). Subsequent calls are faster. If the verifier is temporarily unavailable, the component surfaces the error honestly rather than returning a fake result.