the full verifier, running in your browser
warming up — verification starts automatically
The actual Dafny verifier — Dafny 4.11 and Boogie 3.5.5, the same assemblies the CLI runs — executing on the .NET runtime compiled to WebAssembly. Boogie normally pipes SMT-LIB to a Z3 subprocess; here that pipe is rerouted into Z3 wasm. Everything — parsing, resolution, verification-condition generation, solving — happens on your machine.
It verifies as you type: parse and type errors appear inline almost immediately, and the full pipeline — every proof obligation discharged by Z3, with a 15-second solver limit each — re-runs whenever you pause. If it verifies, that's a proof about all inputs — not a test suite.