papers/lux-model-checking-tla/sections/07-from-specification-to-implementation.tex

\section{From Specification to Implementation}


The TLA+ specification is not the implementation. It is a \emph{model} of the
implementation. The gap between specification and implementation is where bugs hide.

\subsection{Specification-Guided Testing}

Use TLC traces as test scenarios. For every counterexample found during specification
development, write a Go integration test that reproduces the exact message sequence.

\begin{lstlisting}[language=Go,caption={Go test derived from TLC counterexample trace}]
func TestWaveLivenessBug1(t *testing.T) {
    // From TLC trace: simultaneous conflicting proposals
    net := NewTestNetwork(4, 1) // 4 validators, 1 faulty

    // Faulty proposer sends conflicting blocks
    net.FaultyPropose(0, "B1", []int{1, 2})  // to v1, v2
    net.FaultyPropose(0, "B2", []int{3})      // to v3

    // Deliver messages in order that caused deadlock
    net.Deliver(1, "PROPOSE")
    net.Deliver(2, "PROPOSE")
    net.Deliver(3, "PROPOSE")

    // All honest validators should eventually decide
    for _, v := range net.HonestValidators() {
        require.Eventually(t, func() bool {
            return v.HasDecided()
        }, 10*time.Second, 100*time.Millisecond)
    }
}
\end{lstlisting}

\subsection{Bisimulation}

For critical protocols, maintain a \emph{bisimulation} between the TLA+ specification
and the Go implementation: a mapping from Go states to TLA+ states such that every
Go transition corresponds to a TLA+ transition. This is not formal verification (that
would require Lean~4), but it provides strong confidence that the implementation follows
the specification.

%% ============================================================