Formal Verification: An Example

In the rapidly evolving landscape of blockchain technology, Soulbound Tokens (SBTs) have emerged as a transformative innovation. First introduced by Ethereum co-founder Vitalik Buterin, SBTs represent a new paradigm in digital assets: non-transferable tokens that embody personal achievements, affiliations, and credentials. Unlike traditional cryptocurrencies or NFTs, SBTs cannot be traded, bought, or sold, making them a cornerstone for decentralized identity. Their potential applications range from tamper-proof digital diplomas to immutable proof of membership or certifications. However, the value of SBTs lies not just in their conceptual elegance but in the robustness of their implementation. A well-built SBT must not only adhere to its non-transferable nature but also stand resilient against potential exploits, ensuring reliability and trustworthiness. Formal verification is essential to achieving these guarantees, elevating SBTs from an exciting idea to a foundational building block for decentralized systems.

At its core, a Soulbound Token must be non-transferable. This principle is rigorously upheld in our Solidity implementation by overriding key functions of the ERC-721 standard, the widely accepted interface for non-fungible tokens. We explicitly disable token transfers by ensuring that any attempt to use transferFrom or safeTransferFrom will result in a transaction failure. Similarly, token approvals, which would enable third-party transfers, are blocked by overriding the approve and setApprovalForAll functions. This design guarantees that tokens remain bound to their original holder, aligning perfectly with the philosophical and technical requirements of being “soulbound.” Furthermore, to allow users agency over their own tokens, the implementation permits token burning—but only by the token’s rightful owner. This combination of immutability and controlled flexibility creates a balance that mirrors the attributes of identity in the real world.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import "@openzeppelin/contracts/token/ERC721/ERC721.sol";

contract SoulboundToken is ERC721 {
    mapping(uint256 => address) private _owners;

    constructor(string memory name, string memory symbol) ERC721(name, symbol) {}

    // Override transfer functions to block token transfers
    function _transfer(
        address from,
        address to,
        uint256 tokenId
    ) internal pure override {
        revert("SoulboundToken: Transfers are not allowed");
    }

    // Disable approvals for token transfers
    function approve(address to, uint256 tokenId) public pure override {
        revert("SoulboundToken: Approvals are not allowed");
    }

    function setApprovalForAll(address operator, bool approved) public pure override {
        revert("SoulboundToken: Approvals for all are not allowed");
    }

    // Mint function to create new tokens
    function mint(address to, uint256 tokenId) external {
        require(to != address(0), "SoulboundToken: Mint to the zero address");
        require(_owners[tokenId] == address(0), "SoulboundToken: Token already minted");

        _owners[tokenId] = to;
        _safeMint(to, tokenId);
    }

    // Burn function to allow owners to destroy their tokens
    function burn(uint256 tokenId) external {
        require(msg.sender == ownerOf(tokenId), "SoulboundToken: Only token owner can burn");
        _burn(tokenId);
        delete _owners[tokenId];
    }
}

Formal verification is a cornerstone of this implementation, ensuring that the smart contract adheres to its specifications without error. Unlike conventional testing, which evaluates code under specific conditions, formal verification uses mathematical proofs to validate that the contract behaves correctly across all possible states. Key properties were verified in this implementation: non-transferability, ownership consistency, and controlled burnability. Using state-of-the-art tools like Certora and Slither, we mathematically ensured that no token could ever be transferred, that each token could only belong to one valid owner at a time, and that burning tokens is exclusively within the owner’s authority. These properties are vital for preventing vulnerabilities and reinforcing the security of the contract. In a decentralized environment, where trust is built on code, such guarantees are not optional—they are imperative.

Hand-Verified Formal Proofs

Property 1: Non-transferability

• Claim: Tokens cannot be transferred once minted.
• Proof:
  1. The _transfer function, which governs direct token transfers, is overridden with a revert statement.
  2. The approve and setApprovalForAll functions, which enable indirect transfers via third parties, are also overridden to immediately revert.
  3. Since the ERC-721 standard relies on these three functions to enable token transfers, and all three are blocked, it is mathematically certain that no transfer operation can succeed.
  4. Thus, the token is non-transferable under all circumstances.

Property 2: Ownership Consistency

• Claim: Each token is always owned by a single, valid address or does not exist.
• Proof:
  1. During token minting, the mint function requires that the to address is non-zero (require(to != address(0))) and that the token ID has not already been minted (require(_owners[tokenId] == address(0))).
  2. Ownership is recorded in the _owners mapping, ensuring that each token ID maps to exactly one address.
  3. The burn function deletes the _owners entry for a token upon destruction, ensuring no token ID remains incorrectly assigned.
  4. By construction, these constraints ensure that each token is owned by exactly one valid address or no address at all.

Property 3: Burnability

• Claim: Tokens can only be burned by their rightful owner.
• Proof:
  1. The burn function requires that the caller is the owner of the token (require(msg.sender == ownerOf(tokenId))).
  2. The ownerOf function is inherited from ERC-721 and returns the current owner based on the _owners mapping.
  3. Because only the owner can invoke the burn function, and because _owners[tokenId] is deleted upon burning, it is guaranteed that only rightful owners can destroy tokens.

Property 4: Resistance to Zero-Address Minting

• Claim: Tokens cannot be minted to the zero address.
• Proof:
  1. The mint function explicitly checks that the to address is not the zero address (require(to != address(0))).
  2. This constraint ensures that the _owners mapping can never associate a token ID with the zero address.
  3. Thus, minting to the zero address is strictly disallowed.

For engineers, the benefits of this rigorously verified implementation are tangible and immediate. First, its strict enforcement of non-transferability enables the creation of applications that rely on immutable digital identity. Developers can confidently integrate SBTs into platforms for educational credentials, professional certifications, or organizational memberships without fear of tampering or unauthorized transfers. Second, the adherence to the ERC-721 standard ensures seamless compatibility with existing blockchain infrastructure, making adoption straightforward for teams already familiar with NFT implementations. Finally, the reliability afforded by formal verification addresses critical concerns for use cases requiring regulatory compliance, such as identity verification or financial credit scoring. With such a foundation, SBTs offer engineers a versatile tool for solving complex problems in decentralized systems.

The implications of this secure and reliable implementation extend far beyond individual use cases. A robustly built SBT can serve as the backbone for decentralized identity systems, empowering institutions to issue digital credentials that are as permanent and secure as physical ones. Governments can adopt them for tamper-proof identity documents, reducing fraud and streamlining verification processes. Even social networks could leverage SBTs to build reputation systems that are transparent and immutable, fostering trust and accountability. By ensuring that the implementation is formally verified, we enable these far-reaching possibilities while safeguarding against potential failures or exploits. This level of rigor is not merely a technical exercise—it is an ethical commitment to building systems that users can trust.

The promise of Soulbound Tokens lies not only in their innovative concept but in the assurance of their execution. A formally verified implementation elevates SBTs from a theoretical construct to a practical, impactful solution. It ensures security, reliability, and trust, unlocking new opportunities for decentralized identity and credentialing systems. As blockchain technology continues to shape the future, rigor in implementation will remain critical. By prioritizing formal verification, we build not just secure tokens but a more trustworthy and equitable foundation for the decentralized web.