Commit

i think what you're looking for is conformance checking, but tla only works on the spec itself (lint, format, run TLC). it doesn't read Rust code. TLA+ has no built-in way to check code against a spec. the usual options: - trace validation: log state changes from your Rust code, then have TLC check each trace against the spec - model-based testing: generate traces from the spec with TLC or Apalache, then replay them as tests against your Rust code - Stateright, if you'd rather model-check in Rust directly there's also Quint Studio (in beta, waitlist at quint.sh/waitlist), which aims at checking code against the spec.