enhancement: Narwhal-Tusk spec is only partially faithful — no Byzantine behavior

[danwt]

Summary

The Narwhal-Tusk showcase spec (specl/examples/showcase/narwhal_tusk.specl) models the structural DAG construction and Tusk commit rule but omits Byzantine behavior, making it a partial rather than complete BFT verification.

What's modeled

• DAG construction with quorum-based certificates (round advancement requires 2f+1 certs from previous round)
• Signature collection with quorum requirement
• Tusk deterministic leader election and commit rule (strong path: 2f+1 certs at round r+1)
• No-equivocation invariant (one cert per validator per round)
• Commit agreement (only the deterministic leader commits)

What's missing

1. Byzantine behavior: No equivocating validators, no signature withholding, no invalid certificates. The current model only verifies the happy path.
2. Explicit references: References are implicit (round r certs reference ALL certs from round r-1). The real protocol has explicit reference sets, which matters for causal ordering under Byzantine behavior.
3. Causal commitment: The MarkAncestorCommitted action is commented out to reduce state space. Without it, we can't verify that committing a leader cert correctly commits its entire causal history.

Impact

The spec is fine as a structural reference for how Narwhal-Tusk works, and it does verify the DAG validity and commit agreement properties. But it doesn't provide the full BFT verification that the protocol claims (safety under f Byzantine validators out of 3f+1).

Suggested improvements

1. Add GoFaulty action (similar to the CometBFT spec) allowing up to F validators to go Byzantine
2. Add Byzantine actions: equivocating certificates, arbitrary signing
3. Make references explicit (Dict[Seq[Int], Set[Seq[Int]]] or similar) to properly model causal ordering
4. Re-enable MarkAncestorCommitted with explicit references
5. Verify Agreement holds even with F Byzantine validators

This would bring it to the same level of faithfulness as the CometBFT spec, which models Byzantine prevotes, precommits, and proposals.

[danwt]

Added Byzantine fault model: GoFaulty, ByzantineCreateCert, ByzantineSign actions. Honest actions require not-faulty guards. HonestDAGValidity invariant excludes faulty validators. FaultyBounded invariant. Verified with N=2 F=0 (932 states) and N=3 F=1 (108K+ states, no violations found).