@younes-io I see you're the author of https://github.com/younes-io/tla so I guess you're the person who can answer this. how to verify rust implementation of TLA+ spec?
GitHubGitHub - younes-io/tla: TLA+ CLI for linting, formatting, and TLC checksTLA+ CLI for linting, formatting, and TLC checks - younes-io/tla
commit f9fbe55
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…