# Runnable documentation examples

These 33 models accompany the guides at https://verifpal.com/docs/introduction.
Each model is complete. Download it and run it with Verifpal, or use the
Workbench links in https://verifpal.com/docs/examples.

```sh
verifpal verify accepted-key.vp --sessions 2
verifpal verify scuttlebutt-public.vp --format html > report.html
```

`manifest.json` records expected result codes at one and two sessions, the
fragments forming each base model, and the exact edits defining each variant.
Its version field identifies the verifier used to check those expectations.
Read the full trace, assumptions and search envelope with every result code.

From a checkout of the website, check source consistency and the ordinary
regressions with Node 22.7 or newer:

```sh
node --test tests/*.test.mjs
```

Check all models against the shipped WebAssembly through the production worker:

```sh
node scripts/check-doc-examples.mjs
```

The browser engine uses two sessions. To check both documented session counts
with a native verifier:

```sh
node scripts/check-doc-examples.mjs --native /path/to/verifpal
```

The checks reconstruct base models from the HTML's `data-model-fragment` code
blocks, apply the manifest's variant edits, and compare model tokens with the
downloads. They reject changed verdicts and unconfirmed-witness notes. They do
not need the former PDF manual repository or any third-party Node packages.

After changing a model, update its displayed fragments, download, variant edits,
and Workbench share links together. Run both checks, inspect every changed trace,
and update an expectation only when the change is understood. The Workbench links
contain the complete model in a URL fragment; no model is sent to a server.

The models retain their source license headers: CC-BY-NC-ND-4.0, except for the
adapted upstream `scenarios.vp`, which is GPL-3.0-only. The checker is GPL-3.0-only.