Formal Verification of SSV Protocol

A detailed grant document is provided here.


The Secret Shared Validator (SSV) protocol has been designed by the Ethereum Foundation (in collaboration with others) to build redundancy in the Eth2 Client architecture by removing any possible single point of failure. It is therefore fundamental that the SSV protocol design is free from any security vulnerability to ensure that it functions as designed and does not potentially open up attack vectors to Eth2 Clients operated by honest staking accounts.

The grant work will be carried out by Roberto Saltini’s formal methods team at Consensys. Their previous experience include research on IBFT consensus and the design and formal verification of QBFT consensus.

Grant Details

This grant work proposes to provide the SSV protocol design with:

  • a formal specification and
  • a formal machine-checkable proof that the SSV protocol, as defined by the formal specification, provides the required properties.

The properties to be proven will include the following:

  • Provided that at least 1/3 of the SSVN-VC pairs are honest, then the Validator will never be slashed
  • The protocol never ends up in a deadlock state where no progress can be made
  • Assuming some level of network synchrony, a new attestation/block signature will always be eventually produced.

Grant Amount

This grant is co-funded by an equal split between 3 parties (incl. Ethereum Foundation). The total grant amount is USD 188k, which puts each party’s share at USD 62.7k.



This is very important!



1 Like

The grant for the spec was successfully voted on by the DAO.


Thank you DAO for approving the grant.

Please use the following address for the grant payment.


ETH is preferred over USDC if possible.

Thank you.


I can confirm Roberto sent me that address as well.

For the records:
The first version of the spec is now available on GitHub. Congrats, everyone!:tada:
ethereum/distributed-validator-specs: Ethereum Distributed Validator Specifications (