Applying Formal Methods to Hyperledger Fabric Chaincodes: The BaseToken Case

HLF

Hyperledger Fabric (HLF) is one of the most popular enterprise blockchain platforms where business logic is implemented in the form of smart contracts, also known as chaincodes. Chaincodes are implemented in general-purpose languages such as Go, JavaScript, or Java. Errors at the chaincode level, that is, at the level of business logic, can lead to enormous financial and reputational losses. Unlike Ethereum and Bitcoin, Hyperledger Fabric is a permissioned platform: a limited list of counterparties is allowed to the network. However, errors in the chaincode still impact money and reputation, so the fact that "this is not a public blockchain" does not globally protect against critical bugs.

In my previous article on formal verification of smart contracts in Ethereum, I discussed in detail what formal verification methods are and why they are important in the context of blockchain security. In brief: formal methods allow for a strict mathematical proof of the correctness of the program code concerning specified properties. In the context of blockchain, this means that vulnerabilities can be detected in advance or their absence can be strictly proven. The relevance of formal verification of smart contracts lies in the fact that auditing and testing smart contracts can uncover errors but do not guarantee their absence.

Foundation: a framework for chaincode under HLF

The Foundation framework is a Go library that simplifies the development of chaincodes for Hyperledger Fabric and is used in Russian CFA platforms. Foundation provides ready-made primitives — such as BaseToken and BaseContract — and unified approaches to routing calls, as well as utility functions, so you don't have to write infrastructure code from scratch. The basic building block is BaseContract: it stores the call environment (stub, tracing), holds the method router, and provides standard service requests like a list of available functions, acting as a common layer for any smart contracts based on Foundation.

BaseToken is built on top of BaseContract: the BaseToken structure embeds it and adds the storage of token configuration (issuer, fee parameters, limits) in the global state, as well as methods for handling emission and token parameters. Calls are automatically routed by method name: all public functions with the prefixes Tx and Query become transactional and reading entry points, while the first argument sender includes rights checks; the reflect-router parses the arguments itself and calls the required method without manual parsing.

Thus, the BaseToken chaincode provides standard token functionality on the Hyperledger Fabric platform — storing participant balances, token issuance operations, transfers from one account to another, setting and collecting fees, burning tokens, etc. Our task was to use formal verification to ensure that this implementation is secure and free of bugs.

Formal Verification of Chaincodes

So, our goal was to formally verify the BaseToken chaincode, that is, to prove that its behavior meets a set of essential security and correctness requirements, as well as to formulate these requirements in the form of a formal specification.

The first thing that needed to be done was to choose an approach and a tool for verification. We settled on the model checking method, which we had previously used for the formal verification of consensus protocols. This choice was made, firstly, for architectural reasons. The architecture of HLF differs significantly from the architecture of public blockchains, which complicates the use of existing frameworks for modeling and deductive verification, most of which were developed for Ethereum (for example, Concert). Chaincodes are essentially regular programs written in Golang, however, mature tools covering all possible constructs of the language for the formal verification of programs in this language have not yet been developed. Goose and coq-of-go only support subsets of Go, which are insufficient for analyzing the selected chaincodes. In addition, the model checking method is less labor-intensive than deductive verification.

For modeling and verification, TLA⁺ and Apalache Model Checker were chosen, respectively. A model in TLA⁺ is a set of states and transitions between these states, defined in terms of predicates and actions. The model describes the behavior of the system as a sequence of states that satisfy logical conditions and change as a result of actions. Programs written in TLA⁺ are not executed by the computer like programs in conventional programming languages: they are run through a model checker. A model checker is a program that explores all possible execution paths of the system. The user specifies the behavior and property, and the model checker verifies whether they hold for the given model or not. In case the property is violated, the tool provides a counterexample.

In order to write a model in TLA⁺, it is necessary to define the initial state and the transition system. The model can be verified for property satisfaction by specifying these properties as predicates and running a model checker.

Building a formal model of chaincode

Now let's move on to building a formal model of the behavior of BaseToken, abstracting from the specific Go code, while manually translating the key logic.

Standard chaincode in HLF must implement an interface consisting of the Init and Invoke methods:

type Chaincode interface {
  // Init is called during Instantiate transaction
  Init(stub ChaincodeStubInterface) pb.Response

  // Invoke is called to update or query the ledger
  Invoke(stub ChaincodeStubInterface) pb.Response
}

BaseToken does not directly declare Init/Invoke: it embeds core.BaseContract and implements core.BaseContractInterface. This implementation is passed to core.NewCC, and the calls to Init/Invoke go through the Chaincode structure, where Init and Invoke are implemented. It is created via core.NewCC, sets up the router for the contract methods, and contains a field contract of type BaseContractInterface.

Let’s consider the main aspects of modeling.

• State model: we defined state variables reflecting the key elements of the Fabric ledger. In the case of a token, these primarily include account balances and related parameters (total token issuance, exchange rates, limits, and fees).

VARIABLES
    \* @type: Str -> Int;
    tokenBalances,
    \* @type: <> -> Int;
    allowedBalances,    \* [address: Address, currency: Currency] -> Nat
    \* @type: Int;
    totalEmission,
    \* @type: <> -> Int;
    rates,              \* [dealType: String, currency: Currency] -> Rate
    \* @type: <> -> $limit;
    limits,             \* [dealType: String, currency: Currency] -> [min: Nat, max: Nat]
    \* @type: $feeRecord;
    fee,                \* [currency: String, rate: Nat, floor: Nat, cap: Nat]
    \* @type: Str;
    feeAddress

• The initial state models the call to Init, that is, it initializes the variables. We assume that in the initial state all token balances are zero, while the balances in fiat currencies equal 1000.

Init ==
    /\ tokenBalances = [a \in Addresses |-> 0]
    /\ allowedBalances = [ac \in Addresses \X Currencies |->
            IF ac[1] # Issuer /\ ac[1] # FeeAddress THEN 1000 ELSE 0]
    /\ totalEmission = 0
    /\ rates = [dc \in DealTypes \X Currencies |-> 0]
    /\ limits = [dc \in DealTypes \X Currencies |-> [min |-> 0, max |-> 0
    /\ fee = [currency |-> "TOKEN", rate |-> 0, floor |-> 0, cap |-> 0]
    /\ feeAddress = FeeAddress

• Accounting for Rights and Roles: roles of users have been introduced in the model according to the original logic of BaseToken. Issuer owns the emissions and rates and has unique rights to call the functions TxSetRate, TxSetLimits, TxDeleteRate, TxBuyToken/TxBuyBack. Fee_setter can call TxSetFee, that is, set the transaction fee. Fee_address_setter can call TxSetFeeAddress, setting the address for receiving fees. The core of the Foundation implements an access matrix and defines the roles acl.Issuer, acl.FeeSetter, allowing queries to the ACL about rights (GetAccountRight, IsIssuerAccountRight), but the BaseToken does not currently use them: access control is implemented through static addresses in the configuration and checks sender.Equal.

Hyperledger Fabric Abstractions: the Hyperledger Fabric environment itself (transaction mechanism, execution order, confirmations) was omitted in the verification process. We assume sequential execution of transactions (that is, we rely on the correct operation of the Orderer Service, responsible for their ordering) and focus directly on the business logic of the chaincode.

Transaction Model: the main methods of the considered chaincode TxTransfer, TxBuyToken, TxBuyBack, EmissionAdd, EmissionSub, TxSetRate, TxSetLimits, TxDeleteRate, TxSetFee, TxSetFeeAddress were expressed as transitions between states. Each transition has preconditions and an effect on the state. We carefully laid down these rules according to the original implementation of BaseToken, having first conducted a manual audit of its logic. For clarity, let’s consider an example of the model of the function TxBuyToken, to understand how the actual code maps to the verifiable model. TxBuyToken is intended for purchasing tokens with fiat currency (allowed currency): it checks that the buyer is not the issuer, and limits are also checked; in the case of successful checks, the exchange occurs at the current rate from the state.

func (bt *BaseToken) TxBuyToken(sender *types.Sender, amount *big.Int, currency string) error {
	if sender.Equal(bt.Issuer()) {
		return errors.New("impossible operation")
	}

	if amount.Cmp(big.NewInt(0)) == 0 {
		return errors.New(ErrAmountEqualZero)
	}

	price, err := bt.CheckLimitsAndPrice("buyToken", amount, currency)
	if err != nil {
		return err
	}

	if err = bt.AllowedBalanceTransfer(currency, sender.Address(), bt.Issuer(), price, "buyToken"); err != nil {
		return err
	}

	return bt.TokenBalanceTransfer(bt.Issuer(), sender.Address(), amount, "buyToken")
}

BuyToken(buyer, amount, currency) ==
    /\ buyer # Issuer
    /\ amount > 0
    /\ rates[<<"buyToken", currency>>] > 0
    /\ InLimits(amount, "buyToken", currency)
    /\ amount <= tokenBalances[Issuer]
    /\ LET price == CalcPrice(amount, "buyToken", currency)
       IN /\ price <= allowedBalances[<>]
          /\ tokenBalances' = [tokenBalances EXCEPT
                ![Issuer] = @ - amount,
                ![buyer] = @ + amount]
          /\ allowedBalances' = [allowedBalances EXCEPT
                ![<>] = @ - price,
                ![<>] = @ + price]
    /\ UNCHANGED <>

Specification of properties for verification

We will define the key properties that the token must satisfy. We will provide just a few examples of the specification of the properties being verified; the complete formal specification of BaseToken in TLA⁺ can be found in our repository.

• Preservation of balance: the total aggregate balance across the entire system remains consistent. The sum of all token balances equals the total emission, meaning tokens are neither created nor destroyed in any way other than through the operations EmissionAdd and EmissionSub.

Let's consider an example of the specification of this property in TLA⁺.

AddBalance(sum, addr) == sum + tokenBalances[addr]

TotalTokenBalance == ApaFoldSet(AddBalance, 0, Addresses)

TotalBalanceEqualsEmission ==
    TotalTokenBalance = totalEmission

The operator ApaFoldSet(Op, b, C) works like a fold over a set: it takes an initial value of the accumulator b and sequentially applies a binary operator (in our case — addition) to all elements of the set C in some order. If the set is non-empty, the result is defined by recursion of the form ApaFoldSet(Op, b, C) = ApaFoldSet(Op, Op(b, x), C \ {x}) for some element x ∈ C.

• Lack of negative balances: No account can have a negative token balance as a result of any sequence of operations. Emission, exchange rates, fees, and limits must also not be negative in any system state.

BalancesNonNegative ==
    /\ \A a \in Addresses: tokenBalances[a] >= 0
    /\ \A a \in Addresses, c \in Currencies: allowedBalances[<>] >= 0

• Only the issuer can change the emission. If the emission changes, then the difference goes (comes) to the Issuer's balance; no one else can "create" tokens for themselves.

EmissionAuthorization ==
    totalEmission' # totalEmission =>
        tokenBalances'[Issuer] - tokenBalances[Issuer] = totalEmission' - totalEmission

• Correctness of transfers and purchase operations: Tokens can only be transferred between accounts if the necessary conditions are met (for example, the sender has sufficient funds and the balances are updated correctly after the transaction).

BuyConsistency ==
    \A a \in Addresses, c \in Currencies:
        (a # Issuer
         /\ allowedBalances'[<>] < allowedBalances[<>]
         /\ tokenBalances'[a] > tokenBalances[a]) =>
    /\ InLimits(tokenBalances'[a] - tokenBalances[a], "buyToken", c)
    /\ rates[<<"buyToken", c>>] > 0
    /\ allowedBalances[<>] - allowedBalances'[<>] =
        (tokenBalances'[a] - tokenBalances[a]) * rates[<<"buyToken", c>>]

Note the variables with a dash. Invariants containing such variables are called action invariants and are checked by the model checker not in every state, but on any pair of neighboring states. That is, in the pair (s, s’), s’ is the value of the variable s in the next state. In our case, this is convenient for verifying the correctness of operations like Transfer: we need to link the old and new states, not just look at snapshots. The ability to verify such properties is an advantage of the Apalache tool over the more classic TLC Model Checker.

Before we start model checking, we need to set the values of all constants. To avoid combinatorial explosion of the number of states, we will check the model with no more than five addresses and two fiat currencies. The limitation of the verification scope helps make model checking feasible in a reasonable time without sacrificing the verification of important cases.

After the stage of specifying properties and limiting constants, we can proceed to their verification on the model.

Verification Launch and Results

As mentioned above, Apalache was chosen as the verification tool for the constructed TLA⁺ model BaseToken. Apalache is a bounded model checker, meaning it checks a finite number of transitions of the model starting from the initial state. When verifying, we must explicitly specify how many transitions we want to check. Among the advantages of Apalache is the verification of action invariants and trace invariants, as well as the built-in type checker for TLA⁺, which simplifies writing correct models. Another suitable tool is TLC, which checks all possible states of the model. It is evident that our model will have an unlimited number of states (for example, with zero commission, users can infinitely send tokens to each other). We could use TLC in simulation mode or add a counter for the number of transitions in the model, imposing an upper limit on it; however, we preferred to use Apalache due to its more suitable functionality in this case.

After preparing the model and properties, we launched the verification using Apalache. The tool automatically explored all possible sequences of operations (within the specified constraints) and checked that none of the formulated properties were violated. We verified the model with a number of steps up to k=7, as well as in simulation mode with 10,000 traces and k=20 transitions. It is worth noting that folding over sets in the property TotalBalanceEqualsEmission significantly affects performance: each such expression unfolds into non-trivial constraints over all elements of the set, so the size of the participant set directly impacts the verification time. The other invariants are verified much faster.

As a result, none of the checks revealed violations: the BaseToken model satisfies all specified invariants. This means that within the constructed model, covering the verified scenarios and assumptions, the behavior of the smart contract aligns with the specified properties: tokens do not disappear or appear out of thin air, access rights are respected, and invalid actions are prevented.

The absence of counterexamples is an important result: within the constructed model, BaseToken satisfies the stated properties, which significantly reduces the risk of errors in the token's business logic. It is essential to understand the limits of such guarantees. We verified the internal logic of the chaincode under a number of architectural assumptions: that the Hyperledger Fabric platform itself correctly executes transactions, that the environment and ACL return the expected permissions, and that the model abstracts details that do not affect the verified invariants. Furthermore, the verification was conducted on limited parameters and scenario lengths. Nonetheless, even within these constraints, the tool examined thousands of achievable transitions, including edge cases, and found no violations: this is a good signal for developers, but not a guarantee of infallibility for the entire stack and all operational conditions.

Conclusion

Formal verification methods, particularly model checking, have proven their value in practice: they allow for the detection and prevention of errors before deploying code to production. In our case, the verification of the BaseToken chaincode did not reveal logical vulnerabilities, which increases confidence in the correctness of the implementation. However, it is equally important that the verification process itself strengthens the development culture — it forces clear formulation of requirements, understanding of the system's boundaries, and consideration of edge cases.

Our project has provided several valuable insights and results for the Hyperledger Fabric community:

• Demonstration of the capabilities of formal methods for Hyperledger Fabric. We showed that model checking techniques can be successfully applied not only to smart contracts in EVM networks but also to chaincodes on Hyperledger Fabric. This expands the toolkit for ensuring quality in enterprise blockchain development.

• Increased trust in BaseToken. Formal verification significantly enhances confidence in the security and correctness of BaseToken.

For us, this case was a good test: formal methods here did not remain at the theoretical level but turned into a working tool for real chaincode in a real ecosystem. We intend to continue research in this area and apply formal methods to other chaincodes and infrastructure components of Hyperledger Fabric.

Thank you for your attention! If you have any questions or ideas, we would be happy to discuss them in the comments.