[Technical Discussion] TLA+ Verified Safety Invariants for Rust-based BFT Consensus (Sharing my implementation)

Technology
1

Hi everyone,

I’ve been working independently on a Rust-based distributed consensus kernel (Project Mnemosyne) for the past year, focusing on Byzantine Fault Tolerance (BFT) in unstable network environments.

While studying Zcash’s consensus evolution (moving towards PoS/Crosslink), I noticed that state consistency verification is often the bottleneck. I wanted to share a specific approach I used: defining formal invariants in TLA+ first, then mapping them to Rust structs.

Instead of relying solely on unit tests, I modeled the Safety property to ensure that no two honest nodes ever commit different values for the same round, even under 𝑓<𝑛/3 Byzantine faults.

1. The TLA+ Invariant (Model Checked for 10^6 states):

I defined the Safety theorem to enforce strict consistency across the quorum:

---------------- MODULE MnemosyneInvariants ----------------
EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS Processes, Rounds, Values

VARIABLES state, committed

(* Safety Theorem: Linearizability *)
Safety ==
  \A r \in Rounds :
    \A p1, p2 \in Processes :
      (committed[r][p1] # NULL /\ committed[r][p2] # NULL)
      => (committed[r][p1] = committed[r][p2])

(* Liveness: Eventual delivery *)
Liveness ==
  \A v \in Values :
    (\E p \in Processes : proposed[p] = v)
    ~> (\A q \in Processes : committed[q] = v)

============================================================

2. The Rust Implementation (Simplified):

To enforce this Safety invariant at the compiler level, I implemented a QuorumCertificate struct in Rust that requires cryptographic proof aggregation before a Commit state can be instantiated.

Rust

// A simplified view of how I map the TLA+ safety to Rust types

use sha2::{Sha256, Digest};
use ed25519_dalek::{Signature, Verifier, PublicKey};

struct QuorumCertificate {
    block_hash: [u8; 32],
    round: u64,
    // The aggregation of signatures proves > 2/3 participation
    signatures: Vec<(PublicKey, Signature)>,
}

impl QuorumCertificate {
    // This function enforces the "Safety" invariant from TLA+
    // It physically prevents the creation of a QC without a supermajority
    pub fn verify(&self, validators: &[PublicKey]) -> Result<bool, ConsensusError> {
        let weight: usize = self.signatures.iter()
            .filter(|(pk, sig)| validators.contains(pk) && pk.verify(&self.block_hash, sig).is_ok())
            .count();

        if weight * 3 > validators.len() * 2 {
            Ok(true)
        } else {
            Err(ConsensusError::InsufficientQuorum)
        }
    }
}

My Question to the Community:

Has the Zcash dev team considered integrating TLA+ spec-driven development for the upcoming Zcash Shielded Assets or Crosslink protocols?

I have found that this “Formal Method → Rust Code” pipeline significantly reduces logic bugs in edge cases. I’m happy to open-source more of my rigorous verification modules if there is interest in using them for the Zcash network stack.

Looking forward to any technical feedback.

Best,

Han

*(Rust Systems Engineer)
*
https://www.researchgate.net/profile/Bo-Jun-Han
https://osf.io/xdjz8/

ORCID iD: 0009-0001-3067-231