Proof that runs in your browser
Formally verified Ada/SPARK cores, compiled to WebAssembly, refusing malformed input on your own machine. Nothing here is asserted — it is checked.
Ada / SPARKgnatprove, level 2
0 unproved · 0 assumptionsindependently re-proved
wasm32 · runs locally
What you are looking at. Three small components were specified in
English, generated, and then proved — a machine checked every stated property
against the code, exhaustively, for all inputs. The same source was compiled to
WebAssembly. Your browser is now running it. The tables below are computed live by
that verified code, not by this page's JavaScript.
1. A codec that cannot lose your data
The property proved: decoding an encoded record returns exactly the original record, for every possible input. Not sampled — every input.
| Kind | Length | Sequence | Wire bytes | Round trip |
|---|
Loading…
2. A gate that cannot be talked around
Commands arrive as raw bytes from an untrusted interface. The verified gate decides what may proceed. Each refusal below is a named theorem — a property proved once, holding for every input forever, rather than a test that happened to pass.
| Scenario | Session | Command bytes | Verdict | Proved outcome |
|---|
Why it matters. Software that merely passes tests is correct on the
cases someone thought of. Software carrying proofs is correct on the cases nobody
thought of — including the ones an adversary is looking for. The cost of that guarantee
used to be prohibitive. It isn't any more: these components were specified, generated,
proved and independently re-verified in a single working day.