Writing User-Defined TSA Checkers. Part 2

In Part 1 we used TSA to extract a secret from a live contract. In this Part 2, we'll use checkers to find bugs by writing contract invariants and asking TSA to find violations.

You should be familiar with Part 1 (sections 5–7) before proceeding — this guide builds on those concepts.

1. Set Up the Environment

sudo docker pull ghcr.io/espritoxyz/tsa:latest
sudo docker run --entrypoint bash --workdir /home -it ghcr.io/espritoxyz/tsa

mkdir tutorial-2 && cd tutorial-2
npm install @ton/core

mkdir imports
cp ../tsa.jar .
cp /usr/share/ton/smartcont/stdlib.fc imports/
mkdir imports/lib && cp -r /usr/lib/fift/. imports/lib
cd imports
curl -O https://raw.githubusercontent.com/espritoxyz/tsa/refs/heads/master/tsa-test/src/test/resources/imports/tsa_functions.fc
cd ..

2. The Target Contract

We'll analyze a slightly modified version of the Bank contract from the TON hack-challenge-1 repo. It has a non-obvious bug that we'll find through invariant checking.

In /home/tutorial-2, create a file named bank.fc with the following code:

#include "imports/stdlib.fc";
 
() recv_internal(msg_value, in_msg_full, in_msg_body) {
    if (in_msg_body.slice_empty?()) { ;; ignore empty messages
        return ();
    }
    slice cs = in_msg_full.begin_parse();
    int flags = cs~load_uint(4);
 
    if (flags & 1) { ;; ignore all bounced messages
        return ();
    }
    slice sender_address = cs~load_msg_addr();
    (int wc, int sender) = parse_std_addr(sender_address);
    throw_unless(97, wc == 0);
    
    int op = in_msg_body~load_uint(32);
    
    cell accounts = get_data();
 
    if (op == 0) { ;; Deposit
        int fee = 10000000;
        throw_if(98, msg_value < fee);
        int balance = msg_value - fee; 
        (_, slice old_balance_slice, int found?) = accounts.udict_delete_get?(256, sender);
        if (found?) {
            balance += old_balance_slice~load_coins();
        }
        accounts~udict_set_builder(256, sender, begin_cell().store_coins(balance));
    }
 
    if (op == 1) { ;; Withdraw
        (_, slice old_balance_slice, int found?) = accounts.udict_delete_get?(256, sender);
        throw_unless(99, found?);
        int balance = old_balance_slice~load_coins();
        int withdraw_amount = in_msg_body~load_coins();
        throw_unless(100, balance >= withdraw_amount);
        balance -= withdraw_amount;
        if (balance > 0) {
            accounts~udict_set_builder(256, sender, begin_cell().store_coins(balance));
        }
        var msg = begin_cell()
          .store_uint(0x18, 6)
          .store_slice(sender_address)
          .store_coins(withdraw_amount)
          .store_uint(0, 1 + 4 + 4 + 64 + 32 + 1 + 1)
        .end_cell();
        send_raw_message(msg, 64 + 2);
    }
 
    set_data(accounts);
}
 
(int, int) get_account_balance(int account) method_id(70000) {
    (slice balance_slice, int found?) = get_data().udict_get?(256, account);
    if (found?) {
        return (balance_slice~load_coins(), found?);
    } else {
        return (0, found?);
    }
}

The contract stores a dictionary of accounts (keyed by 256-bit address integers) with coin balances. It supports two operations: deposit (opcode 0) and withdraw (opcode 1).

3. Define the Invariants

We would like to check that the Bank contract satisfies the following properties (invariants). These are properties expected of any correct bank implementation — in other words, they form the contract's specification.

1. Deposit invariants:

    (1.a) For any non-existing account A, if the deposit amount covers the fees, then after the deposit A exists as a bank account and final_balance(A) = deposit - fees.

    (1.b) For any existing bank account A, if the deposit amount covers the fees, then after the deposit A still exists and final_balance(A) = prev_balance(A) + (deposit - fees).

    (1.c) It is not possible to deposit an amount smaller than the fees.

2. Withdraw invariants:

    (2.a) For any existing bank account A, if the withdraw amount does not exceed the current balance, then after the withdrawal A still exists and final_balance(A) = prev_balance(A) - withdraw_amount.

    (2.b) For any existing bank account A, it is not possible to withdraw an amount that exceeds the current balance.

    (2.c) It is not possible to withdraw from a non-existent bank account.

Since TSA works as an "example finder", we will use it to look for examples that violate the invariants. If we find one, we have found a bug.

The strategy: negate each invariant and encode the negation as a checker contract. If TSA finds an input that triggers the checker's throw_if, it has found a violation.

This tutorial focuses on building checkers for invariants (1.a) and (2.a) to illustrate the approach.

4. Write the Checker for Invariant (1.a)

Let us start by writing invariant (1.a) a bit more formally:

For any account id A and deposit amount d, if A is not in Accounts, and d >= fees, and the deposit message successfully executes, then immediately afterwards, A is in Accounts and balance(A) = d - fees.

Here, Accounts is the accounts dictionary currently active in the bank, fees is the fixed amount 10000000, and balance(A) is the current balance of account id A in Accounts.

The objective is to find violations to the above sentence.

The first step is to negate the sentence. After pushing the negation inside the sentence, we obtain:

There is an account id A and deposit amount d, such that A is not in Accounts, and d >= fees, and immediately after the deposit message successfully executes, either A is not in Accounts or balance(A) != d - fees.

In /home/tutorial-2, create a file named checker_1a.fc:

#include "imports/stdlib.fc";
#include "imports/tsa_functions.fc";
 
const int fees = 10000000;
 
global int deposit_amount;
global int account_id;
 
() on_internal_message_send(int balance, int msg_value, cell msg_full, slice msg_body, int message_id) impure method_id {
    ;; Constrain the sender address to match our account id.
    slice cs = msg_full.begin_parse();
    cs~load_uint(4);
    slice sender_address = cs~load_msg_addr();
    (_, int sender_addr_int) = parse_std_addr(sender_address);
    tsa_assert(account_id == sender_addr_int);
 
    ;; Must be a deposit message.
    int op = msg_body~load_uint(32);
    tsa_assert(op == 0);
 
    ;; Message value equals deposit amount, and covers fees.
    tsa_assert(deposit_amount == msg_value);
    tsa_assert(deposit_amount >= fees);
}
 
() main() impure {
    tsa_forbid_failures();
 
    account_id = tsa_mk_int(256, 0);
    deposit_amount = tsa_mk_int(100, 0);
 
    ;; Pre-condition: account does NOT exist yet.
    cell bankAccounts = tsa_get_c4(1);
    (_, int current_found?) = bankAccounts.udict_get?(256, account_id);
    tsa_assert(~ current_found?);
 
    ;; Send the deposit.
    tsa_send_internal_message(1, 0);
 
    ;; Read post-state.
    (int new_balance, int new_found?) = tsa_call_2_1(account_id, 1, 70000);
 
    tsa_allow_failures();
 
    tsa_fetch_value(deposit_amount, 1);
    tsa_fetch_value(new_balance, 2);
    tsa_fetch_value(account_id, 3);
    tsa_fetch_value(new_found?, 4);
 
    ;; Negated invariant: account missing OR balance wrong.
    int disj1 = ~ new_found?;
    int disj2 = new_balance != (deposit_amount - fees);
    throw_if(257, disj1 | disj2);
}

Key concepts used here:

• tsa_get_c4(contract_id) returns the contract's persistent state (the accounts dictionary).
• on_internal_message_send is an event handler that fires before each tsa_send_internal_message. Use it to constrain the message (opcode, sender, value, etc.).
• tsa_assert(condition) tells TSA to only keep symbolic instantiations where the condition holds.

5. Write the Checker for Invariant (2.a)

Again, let us start by writing invariant (2.a) a bit more formally:

For any account id A and withdraw amount w, if A is in Accounts, and prev_balance(A) >= w, and the withdraw message successfully executes, then immediately afterwards, A is in Accounts and new_balance(A) = prev_balance(A) - w.

Here, Accounts is the accounts dictionary currently active in the bank, prev_balance(A) is the balance of account id A before the withdraw message, and new_balance(A) is the balance of account id A after the withdraw message.

The objective is to find violations to the above sentence. As was done to invariant (1.a), negate the sentence. After pushing the negation inside the sentence, we obtain:

There is an account id A and withdraw amount w, such that A is in Accounts, and prev_balance(A) >= w, and immediately after the withdraw message successfully executes, either A is not in Accounts or new_balance(A) != prev_balance(A) - w.

In /home/tutorial-2, create the file checker_2a.fc:

#include "imports/stdlib.fc";
#include "imports/tsa_functions.fc";
 
global int withdraw_amount;
global int account_id;
 
() on_internal_message_send(int balance, int msg_value, cell msg_full, slice msg_body, int message_id) impure method_id {
    slice cs = msg_full.begin_parse();
    cs~load_uint(4);
    slice sender_address = cs~load_msg_addr();
    (_, int sender_addr_int) = parse_std_addr(sender_address);
    tsa_assert(account_id == sender_addr_int);
 
    ;; Must be a withdraw message.
    int op = msg_body~load_uint(32);
    tsa_assert(op == 1);
 
    ;; Body contains the withdraw amount.
    tsa_assert(withdraw_amount == msg_body~load_coins());
}
 
() main() impure {
    tsa_forbid_failures();
 
    account_id = tsa_mk_int(256, 0);
    withdraw_amount = tsa_mk_int(100, 0);
 
    ;; Pre-condition: account exists and has sufficient balance.
    cell bankAccounts = tsa_get_c4(1);
    (slice balance_slice, int current_found?) = bankAccounts.udict_get?(256, account_id);
    tsa_assert(current_found?);
    int prev_balance = balance_slice~load_coins();
    tsa_assert(prev_balance >= withdraw_amount);
 
    ;; Send the withdrawal.
    tsa_send_internal_message(1, 0);
 
    ;; Read post-state.
    (int new_balance, int new_found?) = tsa_call_2_1(account_id, 1, 70000);
 
    tsa_allow_failures();
 
    tsa_fetch_value(prev_balance, 1);
    tsa_fetch_value(withdraw_amount, 2);
    tsa_fetch_value(new_balance, 3);
    tsa_fetch_value(account_id, 4);
    tsa_fetch_value(new_found?, 5);
 
    ;; Negated invariant: account missing OR balance wrong.
    int disj1 = ~ new_found?;
    int disj2 = new_balance != (prev_balance - withdraw_amount);
    throw_if(257, disj1 | disj2);
}

6. Run TSA

Run both checkers:

java -jar tsa.jar custom-checker \
  --checker checker_1a.fc --contract func bank.fc \
  --fift-std imports/lib -o report_1a.sarif
 
java -jar tsa.jar custom-checker \
  --checker checker_2a.fc --contract func bank.fc \
  --fift-std imports/lib -o report_2a.sarif

7. Interpret the Results

Invariant (1.a) — Deposit

report_1a.sarif should have an empty "results" list — TSA found no violations. The deposit logic is correct.

Invariant (2.a) — Withdraw

report_2a.sarif should contain a finding with exit code 257. The fetchedValues reveal the pattern:

"fetchedValues": {
  "1": "633825300114114700748351602688",  // prev_balance
  "2": "633825300114114700748351602688",  // withdraw_amount
  "3": "633825300114114700748351602688",  // new_balance (should be 0!)
  "4": "0",                               // account_id
  "5": "-1"                               // found? = true
}

The violation occurs when withdraw_amount == prev_balance. After withdrawal, the balance should be 0, but it remains unchanged.

Root Cause

The withdraw branch uses .udict_delete_get? instead of ~udict_delete_get?:

(_, slice old_balance_slice, int found?) = accounts.udict_delete_get?(256, sender);

The . call doesn't mutate accounts, so the sender's entry is never removed. When balance == withdraw_amount, the final balance is 0, so the guard if (balance > 0) is false and the update is skipped. The account keeps its original balance.

You can confirm this by constraining prev_balance != withdraw_amount in the checker — TSA will find no further violations.

8. The General Strategy

1. State your invariants — what should always be true about your contract?
2. Negate each invariant and encode it as a checker.
3. If TSA finds a violation — you've found a bug. Use tsa_fetch_value to understand the pattern.
4. If TSA finds nothing — inject known bugs to confirm the checker works, and sanity-check your constraints.

Conclusion

In this tutorial you've:

• Used invariant checking to find a subtle bug in a real contract
• Learned to use tsa_get_c4, tsa_assert, and on_internal_message_send for constraining contract state and messages
• Interpreted TSA reports and traced findings back to the root cause in source code

The invariant-based approach scales to any property you can express: authorization, balance conservation, access control, and more.