Add formal verification and harden dictation boundaries

[note89]

Cancellation could leave cleanup or cloud work running, and a delayed insertion could settle a newer session. The Swift and Rust ports also disagreed on large numbers and decomposed accents. This adds executable verification and fixes those failures.

Summary

• Add TLA+ lifecycle models with original-bug counterexamples, kernel-checked Lean scorer proofs, and CI for both. Lean proves its reference algorithm; production agreement is checked through an executable differential bridge.
• Add reproducible algebraic properties, 500 generated session traces, cloud cancellation/audio tests, and 1,013 Swift/Rust contract cases covering scoring, diffs, dictionary rewrites, and cleanup decisions.
• Enforce session ownership and cancellation at asynchronous boundaries, reject content-free cleanup, flush resampler tails, and align numeric ranges and Unicode normalization across ports.

Test plan

• Full Swift suite: 107 tests in 21 suites.
• Rust workspace suite: 33 tests.
• Lean proof audit and 1,013 cross-port comparisons against the executable oracle.
• TLC: 5,036 distinct states; both original counterexamples reproduced.
• Swift products build and bake-off checks; Rust workspace/all-targets check.
• Swift/Rust formatting, shell/Python/fixture syntax, bundle metadata, and whitespace checks.