Verification
The Rust code is fast and untrusted. A small Lean 4 model carries the proofs, runs as an oracle on the same inputs as Rust, and must produce the same traces. This page lists what is proven and how to run every check yourself.
Where the trust sits
The theorems are about the Lean model, not about the Rust code. The bridge between the two is trace equality: Rust runs a chart, records what it did, and the Lean step replays the same chart and inputs and must produce exactly the same configurations, effects and datamodel requests. Nothing is extracted from Lean into Rust.
- A bug in Rust shows up as a trace difference or a failed W3C test, never as a wrong theorem.
- A bug in the Lean model shows up as a failed proof, or as a trace difference that is then settled against the W3C text.
- The proofs quantify over every datamodel answer, so they hold for every datamodel. They do not prove ECMAScript, CEL or any other expression engine correct.
The Lean package
The model lives in lean/vertep-lean, a Lake package pinned to leanprover/lean4:v4.35.0 (in lean-toolchain). It depends on LeanRDF, pinned to commit b407b97424150fec25a1ade514c71ea7abc61b42, for the RDF 1.2 data model and its SHACL Core validator. The library is compiled with warningAsError, so a sorry fails the build.
It contains the chart IR, a WellFormed predicate with a decision procedure proven correct, the executable step of W3C SCXML Appendix D, the RDF projection and its decoder, the type language, and three protocol models (journal, agent, lease). Next to the library, lakefile.lean builds seven executables:
| Executable | Used for |
|---|---|
vertep-oracle | Replays a chart (as N-Quads) with Rust's recorded inputs and answer tape and writes or compares traces |
vt-certify | The checker behind vt certify |
vertep-journal | Judges observations of the Rust journal protocol against the journal model |
vertep-decide | Judges decision outcomes of the Rust agent machine against the agent model |
vertep-lease | Replays cluster fault-injection histories against the lease model |
vertep-types | Checks values against types, to compare with the Rust value checker |
vertep-shapes | Runs LeanRDF's SHACL validator with the chart shapes on N-Quads files, an empirical check of the shapes |
The datamodel as an answer tape
Lean cannot run ECMAScript. So during a Rust run every datamodel request (evaluate this condition, assign this location) and its answer is written to a tape. In the oracle the Lean step must issue exactly the same requests in the same order, and it takes the answers from the tape. A request that differs is a trace difference. For the null datamodel, Lean evaluates In() itself and needs no tape.
What is proven
lean/vertep-lean/VertepTests/Axioms.lean pins the axioms of 78 main theorems. At build time it collects the axioms each one depends on and fails if anything other than propext, Classical.choice and Quot.sound appears. A sorry shows up as the axiom sorryAx, so it fails there too; the file even proves that the gate rejects a deliberate sorry. The main results, grouped:
| Area | Theorems | In words |
|---|---|---|
| Well-formedness | checkWF_iff, violations_eq_nil_iff | The executable check decides WellFormed exactly, and it reports no violated rule exactly when the chart is well-formed. |
| Determinism | step_deterministic, step_deterministic_out, start_deterministic | Equal session, input and answer tape give equal results. |
| Transition selection | transition_selection, select_spec, Select.selected_enabled, …_conflictFree, …_optimal, …_nodup | In every microstep the selected set is enabled, conflict-free and optimal in the sense of SCXML 3.13. |
| Legal configurations | configuration_wellformedness, compound_exclusivity, parallel_completeness, with compile_cwf, exit_legal, entry_legal, Config.reachable_inv and others | For every well-formed chart, every running session reachable by start and step has a legal configuration (SCXML 3.11): no active compound state has two active children, an active parallel state has all its children active. |
| Declared locations | step_requests_declared, start_requests_declared, dynamic_typed_soundness | step never asks the datamodel about an undeclared location or data item. |
| RDF | Rdf.fromRDF_project, Rdf.fromRDF_sound, Rdf.canonical_determined, Rdf.version_determined, and the Rdf.RT.* lemmas | Decoding the projection of a well-formed chart gives back the same chart, under any base IRI; the decoded chart's projection is in the graph; equal charts have equal canonical forms and versions. |
| Certificates | Certify.check_certified_wellFormed | When the checker certifies a chart, that chart is well-formed. |
| Journal protocol | Journal.replay_determinism, replay_no_divergence, replay_equals_live, turn_idempotent, accepted_once, outbox_safe, outbox_complete, no_message_lost, cas_single, turn_cas_exclusive, accepts_iff, reachable_admissible | Over any interleaving of crashes, redeliveries and concurrent activations: replay reproduces each entry, a message id is processed once, every recorded send is dispatched and no unrecorded one is, and of two appends at one position at most one succeeds. |
| Agents | Agent.decider_safety, stale_not_taken, unknown_not_taken, decision_dedup, decision_once, replay_live, chainGrant_mem, grants_do_not_escalate, grant_enforced, ungranted_not_delivered, granted_delivered | A transition taken because of a decision was enabled when it was offered; stale or unknown decisions are never taken; grants never widen down a chain of invocations, and a send outside the grants is not delivered. |
| Leases | Lease.grant_unique, accepted_granted, one_writer_per_epoch, journal_epochs_ordered, shard_epochs_ordered, message_once, stale_append_fenced, frames_ordered, stale_frame_dropped | Per shard and epoch at most one writer's appends are accepted; a writer with a stale epoch is fenced off. |
| Types | Types.check_iff, check_sound, Chain.dedup, JsonSchema.validate_proj, JsonSchema.jsonSchema_agrees | The type checker decides the typing relation exactly, on every declaration block; the JSON Schema projection accepts a JSON value exactly when it has the type. |
The statement of the configuration theorem, from VertepLean/Config/Theorem.lean:
def ConfigurationWellFormedness : Prop :=
∀ c : Chart, WellFormed c → ∀ cc, compile c = .ok cc →
∀ s, Reachable cc s → s.terminated = false → Legal cc s.config
theorem configuration_wellformedness : ConfigurationWellFormedness :=
configuration_wellformedness_of compile_cwf entry_legalProving it was not a formality. The attempt found three bugs in the W3C Appendix D entry algorithm as both cores implemented it, each producing an illegal configuration from a valid chart with history states. All three are fixed in Rust and Lean, with regression tests on both sides. The Rust property test crates/vertep-conformance/tests/config_legality.rs never generated those shapes, which is why the proof, not the test, found them. The protocol models found two more bugs in the Rust runtime (an outbox mark that passed refused sends, and colliding mailbox row IRIs when two nodes share a store), also fixed.
Some limits are deliberate. The type theorems read a pattern as the lexical rule its regular expression encodes; the regular expressions themselves are not proven equal to those rules. Lean decides int on the exact decimal while Rust decides it on an f64, so differential cases stay away from the edges of the signed 64-bit range.
The verification backlog
Every item below is done: the backlog change was archived on 2026-11-12 with all formal-model requirements implemented and verified.
The open items are tracked in openspec/changes/verification-backlog/tasks.md. As that file stands:
| Task | Statement | State |
|---|---|---|
| 2.3 Shapes equivalence | the chart shapes accept the projection of c exactly when WellFormed c | Done. Rdf.Equiv.shapes_equivalence: for every base IRI, the projection of c conforms to the chart shapes exactly when WellFormed c. The shapes are a Lean term that a test checks against vt-chart-shapes.ttl; the proof splits along WellFormed's rules (per-node rules, unique state ids, legal target sets, acyclic history defaults, unique data ids). No counterexample and no shape defect turned up. |
| 4.2 SHACL projection of types | a value's RDF encoding conforms to its type's generated shape exactly when it has the type | Done. Types.Shacl.shacl_agrees: a value's encoding conforms to its type's shape (named types unfolded far enough) exactly when it has the type, also stated against LeanRDF's validator. It assumes distinct union tags and object keys, and that LeanRDF's regular expressions decide the decimal, datetime and IRI patterns as the type checker does (checked on samples, not proven). The shapes Rust publishes for lists use an IRI where SHACL needs a path, so a standard engine skips list members; fixed in task 4.7: list members now carry a vt:listMember predicate, so the shapes use plain predicate paths. |
4.4 Type soundness of step | a well-typed chart, configuration and input give a well-typed datamodel and well-typed output events | Done. Typed.typed_step_soundness and typed_start_soundness: from a typed datamodel, session, input and answer tape, step and start write only typed values, emit typed sends and queue typed events. The theorems take the chart's static typing as given and state each check of check_chart as a property; the datamodel's evaluation enters as a typed answer tape. The proof found six checker bugs, now fixed: a bare <assign> to a required location, idlocation into a non-string location, foreach item and index types, namelist keys, and declared error.* and done.state.* payloads. |
4.5 vt certify for typed charts | certify charts with a vt:types block | Done. The checker reads the vt:types block, derives the type triples as Rust does and hashes them into the version; 1,000 generated typed charts certify under the Rust version. |
| 2.4, 4.6 Annotations and axioms | every theorem traced and its axioms pinned | Partial; waits on the theorems above. |
Until 2.3 is proven, the Rust SHACL validator, the Rust IR validator and the Lean WellFormed agree because they are tested against each other, not because a theorem says so.
Differential testing
Charts cross to Lean as N-Quads of their RDF projection, decoded by the same fromRDF that the round-trip theorem covers, so every differential run also exercises the projection. The Rust side records one JSON Lines record per macrostep: configuration, effects and datamodel requests. Sources of cases:
- Generated charts.
vertep-testkitgenerates well-formed charts and input sequences (crates/vertep-conformance/src/differential.rs). A disagreement is shrunk by proptest to a minimal chart and inputs and stored incrates/vertep-conformance/regressions/, which every run replays. - The IRP suite. Every runnable W3C test runs on Rust with its answer tape recorded; the oracle must give the same trace and verdict.
- Validator against checker. Generated charts, and the same charts broken by one targeted mutation per validation rule, go to both the Rust validator and
vt-certify(tests/certify.rs). - Protocols.
tests/journal_protocol.rsdrives two nodes sharing one journal store through crashes, redeliveries and concurrent activations and hands the observation tovertep-journal.tests/decide_differential.rsfeeds adversarial decisions (stale and forged correlation ids, unknown or unoffered events, bad payloads) to the agent machine and hasvertep-decidejudge the outcomes. The cluster fault-injection test incrates/vertep-cluster/tests/faults.rsreplays its history throughvertep-lease. - Types.
tests/types_differential.rschecks 4,000 generated declaration blocks, types and values with Rust and withvertep-types.
The full differential runs are #[ignore]d in normal test runs and need the Lean executables built. Small smoke samples run with the ordinary tests and skip with a message when the Lean build is missing. Two excerpts from a run of the full set:
cargo test -p vertep-conformance --release --features differential -- --ignored differential Running tests/differential.rs (target/release/deps/differential-ef2090d5e7034e1f)
running 1 test
test differential_generated_charts_agree_with_lean has been running for over 60 seconds
test differential_generated_charts_agree_with_lean ... ok
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 4 filtered out; finished in 67.89s
...
Running tests/lean.rs (target/release/deps/lean-dc4822d7c4aeae49)
running 1 test
test differential_irp_suite_on_lean ... ok
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 2 filtered out; finished in 1.90sVT_DIFF_CASES sets the number of generated cases, and VT_CERTIFY_CHARTS the size of the certify sample.
The W3C IRP conformance suite
The W3C SCXML 1.0 Implementation Report Plan tests are committed under crates/vertep-conformance/suite/, copied from a pinned revision and transformed with pinned XSLT (confEcma.xsl, confCel.xsl); suite/SOURCE records where they came from and suite/SHA256SUMS pins the files, which the gate checks before it runs. Tests run in an in-memory host with several sessions, the SCXML Event I/O Processor and a virtual clock: no real time, no network.
The CEL datamodel runs the same suite through confCel.xsl variants of every datamodel-neutral template. Tests that have no CEL variant are listed with a reason in suite/cel/EXCLUDED.tsv.
The allow-list
Expected failures are listed in crates/vertep-conformance/allow-list.toml, each with the test, the datamodel and a reason. Three rules keep it honest: an allow-listed test that passes fails the run (so stale entries get removed), an entry without a reason is rejected, and an entry naming a test the suite does not have is rejected. Today it has 45 entries, all for optional ECMAScript tests:
| Entries | Reason |
|---|---|
| 30 | The test uses the xpath datamodel, which Vertep does not implement. |
| 12 | The test needs the Basic HTTP Event I/O Processor; the test host has no network. |
| 2 | XML DOM values in the ECMAScript datamodel. |
| 1 | Test 444 changes the datamodel inside a condition; Vertep evaluates conditions against a read-only scope by design (guard purity). |
cargo test -p vertep-conformance --release --test conformance -- --nocapture conformancerunning 1 test
SCXML IRP conformance (rust)
mandatory/cel 155 variants: 155 passed, 0 failed, 0 allow-listed, 0 unexpected passes, 0 not run
mandatory/ecmascript 158 variants: 158 passed, 0 failed, 0 allow-listed, 0 unexpected passes, 0 not run
mandatory/null 1 variants: 1 passed, 0 failed, 0 allow-listed, 0 unexpected passes, 0 not run
manual/cel 6 variants: 0 passed, 0 failed, 0 allow-listed, 0 unexpected passes, 6 not run
manual/ecmascript 9 variants: 0 passed, 0 failed, 0 allow-listed, 0 unexpected passes, 9 not run
optional/cel 9 variants: 2 passed, 7 failed, 0 allow-listed, 0 unexpected passes, 0 not run
optional/ecmascript 63 variants: 18 passed, 0 failed, 45 allow-listed, 0 unexpected passes, 0 not run
gate: OK (every mandatory test passes or is allow-listed)
optional failures (not gating):Every mandatory variant passes. Optional tests are reported but do not gate the build. The run writes target/conformance-report.json with the verdict and reason for every test. To look at a single test, run the irp example, which prints the verdict, the host log and the macrostep trace:
cargo run -p vertep-conformance --release --example irp -- 144== 144/ecmascript: Pass
-- …/crates/vertep-conformance/suite/ecmascript/144/test144.scxml
log vt0 Some("Outcome") Some(String("pass"))
[0] start
Some("foo") [TransitionRef { source: "s0", index: 0 }]
Some("bar") [TransitionRef { source: "s1", index: 0 }]
config []
effect Log { label: Some("Outcome"), value: Some(String("pass")) }
effect SessionDone { data: Undefined, cancelled: false }Pass a datamodel after the test number (-- 144 null) for another variant. The same suite also runs in WebAssembly through vertep-wasm's conformance feature.
vt certify
vt certify asks the Lean model about one chart. It projects the chart to N-Quads and runs the Lean-compiled checker vt-certify on them. The checker decodes the graph with fromRDF, decides WellFormed, recomputes the version IRI from the canonical N-Quads and, if the chart is well-formed, prints a certificate as N-Triples. vt finds the checker through the VT_CERTIFY environment variable or as vt-certify on PATH.
cd lean/vertep-lean && lake build && export VT_CERTIFY=$PWD/.lake/build/bin/vt-certify
vt certify crates/vertep-scxml/tests/corpus/irp_style.scxml<urn:vertep:chart:sha256:ecbe14970fe047ee3144793bdf6f44dfafda66df4ee4d6e7d516d8274dc97390> <https://w3id.org/vertep/vt#certifiedBy> <urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://w3id.org/vertep/vt#Certificate> .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.checkWF_iff" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.violations_eq_nil_iff" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.Rdf.fromRDF_sound" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.step_deterministic" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.transition_selection" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#theorem> "Vertep.step_requests_declared" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#leanToolchain> "leanprover/lean4:v4.35.0" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#leanRdfRevision> "b407b97424150fec25a1ade514c71ea7abc61b42" .
<urn:vertep:cert:sha256:f5925f214474c6aec41628f097652e5c3a31c53ffef8ec27bf99b4eb6441cf1f> <https://w3id.org/vertep/vt#checkerHash> "sha256:0d7f7bd4fcd09ba11157f1090afff34b79f9d86ab0f3b6443454eb9c309d988d" .The certificate names the theorems it relies on, the Lean toolchain, the LeanRDF revision and the SHA-256 of the checker binary. Its own IRI is a hash of its content, so certifying the same chart with the same checker gives the same certificate. vt certify prints the certificate; storing it next to the chart in a graph store is up to you.
| Exit status | Meaning |
|---|---|
| 0 | Certificate printed |
| 1 | The chart is not well-formed (violated rules on standard error), or the checker is not installed |
| 2 | The graph is not the projection of a chart, or its node IRIs are minted under another chart's version |
Without the checker, vt says how to build it:
vt certify: the Lean checker `vt-certify` is not installed.
Build it from the Lean model and put it on PATH, or point VT_CERTIFY at it:
cd lean/vertep-lean && lake build && export VT_CERTIFY=$PWD/.lake/build/bin/vt-certify
No certificate was produced.Typed charts certify as well (backlog 4.5, done 2026-11-12):
$ vt certify crates/vertep-dm-rust/tests/charts/order.scxml
<urn:vertep:chart:sha256:05bdae901f2ef328f81ad649674bac2beab559eac46bae2dbc34db1bdcd2e38f> <https://w3id.org/vertep/vt#certifiedBy> <urn:vertep:cert:sha256:b9adf42734b3ce2e71ac4d6a6cd87569d41aee090031360b377534e298d9665e> .
<urn:vertep:cert:sha256:b9adf427…> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://w3id.org/vertep/vt#Certificate> .
<urn:vertep:cert:sha256:b9adf427…> <https://w3id.org/vertep/vt#theorem> "Vertep.checkWF_iff" .
… (trimmed: five more theorems, the toolchain, the LeanRDF revision and the checker hash)Running the checks
You need the Rust toolchain from rust-toolchain.toml for everything, and elan (which installs the pinned Lean toolchain) for the Lean steps.
| Check | Command |
|---|---|
| Lean build, source scan, axiom pinning | lean/vertep-lean/scripts/check.sh |
| W3C IRP gate (ECMAScript, CEL, null) | cargo test -p vertep-conformance --release --test conformance -- --nocapture conformance |
| Full Rust-against-Lean differential runs | cargo test -p vertep-conformance --release --features differential -- --ignored differential |
| All conformance tests with smoke samples | cargo test -p vertep-conformance --release |
| One IRP test with its trace | cargo run -p vertep-conformance --release --example irp -- <test> [null|cel] |
| Certify one chart | vt certify <chart> |
scripts/check.sh is the Lean CI gate. It builds the library with warnings as errors, scans the sources for sorry, admit, axiom, unsafe, implemented_by and extern, builds the seven executables and the tests, and prints the axioms of every main theorem:
lean/vertep-lean/scripts/check.sh== lake build VertepLean (warnings are errors)
...
== source scan
== lake build vertep-oracle vt-certify vertep-shapes vertep-journal vertep-lease vertep-decide vertep-types
...
== lake build VertepTests (axioms pinned)
...
== #print axioms of the main theorems
'Vertep.checkWF_iff' depends on axioms: [propext, Quot.sound]
'Vertep.execOkB_iff' depends on axioms: [propext, Quot.sound]
'Vertep.step_deterministic' depends on axioms: [propext, Classical.choice, Quot.sound]
...
'Vertep.configuration_wellformedness' depends on axioms: [propext, Classical.choice, Quot.sound]
'Vertep.compound_exclusivity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Vertep.parallel_completeness' depends on axioms: [propext, Classical.choice, Quot.sound]
OK: no sorry, only propext, Classical.choice and Quot.soundThe first run downloads LeanRDF and builds everything, which takes a while; later runs reuse the build.
Under the differential feature a missing Lean build is an error rather than a skip, so build the Lean executables first.
What comes later
Proving the Rust code itself is deferred. The pure step kernel is kept in a style that Aeneas can translate to Lean (no async, no trait objects inside the kernel, no interior mutability, simple loops). When that work starts, a proof that the translated kernel refines the Lean step can replace the oracle for the kernel; the oracle stays for the shell, the datamodels and the stores.
