[EXPERIMENTAL] feat(tracer): add TLA+ formal verification of concurrency invariants

[kakkoyun]

WIP: This still requires a lot work and validation

Using https://github.com/specula-org/Specula

What does this PR do?

Adds TLA+ formal verification for two critical concurrency protocols in dd-trace-go:

• Phase 1 — Span Lifecycle: Verifies lock ordering (span.mu → trace.mu), finish-guard pattern, partial flush lock inversion safety (#incident-46344), and deadlock freedom. TLC explored 4,437 distinct states across 2 goroutines and 3 spans with all 6 invariants passing.
• Phase 2 — GLS Push/Pop: Verifies push/pop pairing, stack depth correctness, no-leak-on-finish, LIFO ordering, and goroutine isolation. TLC explored 159 distinct states with all 8 invariants passing. Directly complements the kakkoyun/orchestrion_gls_leak branch work.

Includes:

• Hand-written TLA+ specs with TLC model configurations
• Extracted Go source files preserving only concurrency-relevant protocol
• Specula pipeline scripts and configuration for automated Go→TLA+ translation
• CI workflow running TLC model checker on every change to formal-verification/
• Documentation covering background, setup, model explanation, and result interpretation

Motivation

dd-trace-go's tracer has complex concurrency invariants (lock ordering, finish-guard, GLS stack pairing) that are currently enforced only by code comments, runtime assertions, and -race testing. The checklocks CI job is disabled pending annotation coverage. Formal verification with TLA+/TLC mathematically proves these invariants hold for all possible interleavings — not just those exercised by tests.

This is experimental infrastructure to explore whether Specula-based formal verification is practical for dd-trace-go's concurrency model.

Related: #4384 (orchestrion GLS leak fix)

Reviewer's Checklist

• Changed code has unit tests for its functionality at or near 100% coverage.
• System-Tests covering this feature have been added and enabled with the va.b.c-dev version tag.
• There is a benchmark for any new code, or changes to existing code.
• If this interacts with the agent in a new way, a system test has been added.
• New code is free of linting errors. You can check this by running make lint locally.
• New code doesn't break existing tests. You can check this by running make test locally.
• Add an appropriate team label so this PR gets put in the right place for the release notes.
• All generated files are up to date. You can check this by running make generate locally.
• Non-trivial go.mod changes, e.g. adding new modules, are reviewed by @DataDog/dd-trace-go-guild. Make sure all nested modules are up to date by running make fix-modules locally.

Unsure? Have a question? Request a review!

[felixge]

Please ping me for approval once this is ready to look at.

[kakkoyun]

Please ping me for approval once this is ready to look at.

Of course. But it is far from ready :)