Cointime

Cointime

Download App
iOS & Android

ERC-20 Properties For Formal Verification

Validated Project

Details on Formal Verification

Some Solidity smart contracts from this project have been formally verified using symbolic model checking. Each contract was compiled into a mathematical model which reflects all its possible behaviors with respect to the property. The model takes into account the semantics of the Solidity instructions found in the contract. All verification results that we report are based on that model.

Technical Description

The model also formalizes a simplified execution environment of the Ethereum blockchain and a verification harness that performs the initialization of the contract and all possible interactions with the contract. Initially, the contract state is initialized non-deterministically (i.e. by arbitrary values) and over-approximates the reachable state space of the contract throughout any actual deployment on chain. All valid results thus carry over to the contract's behavior in arbitrary states after it has been deployed.

Assumptions and Simplifications

The following assumptions and simplifications apply to our model:

  • Gas consumption is not taken into account, i.e. we assume that executions do not terminate prematurely because they run out of gas.
  • The contract's state variables are non-deterministically initialized before invocation of any function. That ignores contract invariants and may lead to false positives. It is, however, a safe over-approximation.
  • The verification engine reasons about unbounded integers. Machine arithmetic is modeled using modular arithmetic based on the bit-width of the underlying numeric Solidity type. This ensures that over- and underflow characteristics are faithfully represented.
  • Certain low-level calls and inline assembly are not supported and may lead to a contract not being formally verified.
  • We model the semantics of the Solidity source code and not the semantics of the EVM bytecode in a compiled contract.

Formalism for Property Specification

All properties are expressed in linear temporal logic (LTL). For that matter, we treat each invocation of and each return from a public or an external function as a discrete time step. Our analysis reasons about the contract's state upon entering and upon leaving public or external functions.

Apart from the Boolean connectives and the modal operators "always" (written []) and "eventually" (written <>), we use the following predicates as atomic propositions. They are evaluated on the contract's state whenever a discrete time step occurs:

  • started(f, [cond]) Indicates an invocation of contract function f within a state satisfying formula cond.
  • willSucceed(f, [cond]) Indicates an invocation of contract function f within a state satisfying formula cond and considers only those executions that do not revert.
  • finished(f, [cond]) Indicates that execution returns from contract function f in a state satisfying formula cond. Here, formula cond may refer to the contract's state variables and to the value they had upon entering the function (using the old function).
  • reverted(f, [cond]) Indicates that execution of contract function f was interrupted by an exception in a contract state satisfying formula cond.

The verification performed in this audit operates on a harness that non-deterministically invokes a function of the contract's public or external interface. All formulas are analyzed w.r.t. the trace that corresponds to this function invocation.

Description of the Analyzed ERC-20 Properties

The specifications are designed such that they capture the desired and admissible behaviors of the ERC-20 functions transfer, transferFrom, approve, allowance, balanceOf, and totalSupply. In the following, we list those property specifications.

Properties related to function transfer

erc20-transfer-revert-zero

Function transfer Prevents Transfers to the Zero Address. Any call of the form transfer(recipient, amount) must fail if the recipient address is the zero address. Specification:

[](started(contract.transfer(to, value), to == address(0)) ==>

<>(reverted(contract.transfer) || finished(contract.transfer(to, value), return

== false)))

erc20-transfer-succeed-normal

Function transfer Succeeds on Admissible Non-self Transfers. All invocations of the form transfer(recipient, amount) must succeed and return true if

  • the recipient address is not the zero address,
  • amount does not exceed the balance of address msg.sender,
  • transferring amount to the recipient address does not lead to an overflow of the recipient's balance, and
  • the supplied gas suffices to complete the call. Specification:

[](started(contract.transfer(to, value), to != address(0) && to != msg.sender && value >= 0 && value <= _balances[msg.sender] && _balances[to] + value < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[to] >= 0 && _balances[msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transfer(to, value), return == true)))

<>(finished(contract.transfer(to, value), return == true)))

erc20-transfer-succeed-self

Function transfer Succeeds on Admissible Self Transfers. All self-transfers, i.e. invocations of the form transfer(recipient, amount) where the recipient address equals the address in msg.sender must succeed and return true if

  • the value in amount does not exceed the balance of msg.sender and
  • the supplied gas suffices to complete the call. Specification:

[](started(contract.transfer(to, value), to != address(0) && to == msg.sender && value >= 0 && value <= _balances[msg.sender] && _balances[msg.sender] >= 0 && _balances[msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transfer(to, value), return == true)))

erc20-transfer-correct-amount

Function transfer Transfers the Correct Amount in Non-self Transfers. All non-reverting invocations of transfer(recipient, amount) that return true must subtract the value in amount from the balance of msg.sender and add the same value to the balance of the recipient address. Specification:

[](willSucceed(contract.transfer(to, value), to != msg.sender && _balances[to] >= 0 && value >= 0 && _balances[to] + value < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[msg.sender] >= 0 && _balances[msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transfer(to, value), return == true ==> _balances[msg.sender] == old(_balances[msg.sender]) - value && _balances[to] == old(_balances[to]) + value)))

erc20-transfer-correct-amount-self

Function transfer Transfers the Correct Amount in Self Transfers. All non-reverting invocations of transfer(recipient, amount) that return true and where the recipient address equals msg.sender (i.e. self-transfers) must not change the balance of address msg.sender. Specification:

[](willSucceed(contract.transfer(to, value), to == msg.sender && _balances[to] >= 0 && _balances[to] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transfer(to, value), return == true ==> _balances[to] == old(_balances[to]))))

erc20-transfer-change-state

Function transfer Has No Unexpected State Changes. All non-reverting invocations of transfer(recipient, amount) that return true must only modify the balance entries of the msg.sender and the recipient addresses. Specification:

[](willSucceed(contract.transfer(to, value), p1 != msg.sender && p1 != to) ==> <>(finished(contract.transfer(to, value), return == true ==> (_totalSupply == old(_totalSupply) && _allowances == old(_allowances) && _balances[p1] == old(_balances[p1]) && other_state_variables == old(other_state_variables)))))

erc20-transfer-exceed-balance

Function transfer Fails if Requested Amount Exceeds Available Balance. Any transfer of an amount of tokens that exceeds the balance of msg.sender must fail. Specification:

[](started(contract.transfer(to, value), value > _balances[msg.sender] && _balances[msg.sender] >= 0 && value < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(reverted(contract.transfer) || finished(contract.transfer(to, value), return == false)))

erc20-transfer-recipient-overflow

Function transfer Prevents Overflows in the Recipient's Balance. Any invocation of transfer(recipient, amount) must fail if it causes the balance of the recipient address to overflow. Specification:

[](started(contract.transfer(to, value), to != msg.sender && _balances[to] + value >= 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[to] >= 0 && _balances[to] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000 && value > 0 && value <= _balances[msg.sender]) ==> <>(reverted(contract.transfer) || finished(contract.transfer(to, value), return == false) || finished(contract.transfer(to, value), _balances[to] > old(_balances[to]) + value - 0x10000000000000000000000000000000000000000000000000000000000000000)))

erc20-transfer-false

If Function transfer Returns false, the Contract State Has Not Been Changed. If the transfer function in contract contract fails by returning false, it must undo all state changes it incurred before returning to the caller. Specification:

[](willSucceed(contract.transfer(to, value)) ==> <>(finished(contract.transfer(to, value), return == false ==> (_balances == old(_balances) && _totalSupply == old(_totalSupply) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables)))))

erc20-transfer-never-return-false

Function transfer Never Returns false. The transfer function must never return false to signal a failure. Specification:

[](!(finished(contract.transfer, return == false)))

Properties related to function transferFrom

erc20-transferfrom-revert-from-zero

Function transferFrom Fails for Transfers From the Zero Address. All calls of the form transferFrom(from, dest, amount) where the from address is zero, must fail. Specification:

[](started(contract.transferFrom(from, to, value), from == address(0)) ==> <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return == false)))

erc20-transferfrom-revert-to-zero

Function transferFrom Fails for Transfers To the Zero Address. All calls of the form transferFrom(from, dest, amount) where the dest address is zero, must fail. Specification:

[](started(contract.transferFrom(from, to, value), to == address(0)) ==> <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return == false)))

erc20-transferfrom-succeed-normal

Function transferFrom Succeeds on Admissible Non-self Transfers. All invocations of transferFrom(from, dest, amount) must succeed and return true if

  • the value of amount does not exceed the balance of address from,
  • the value of amount does not exceed the allowance of msg.sender for address from,
  • transferring a value of amount to the address in dest does not lead to an overflow of the recipient's balance, and
  • the supplied gas suffices to complete the call. Specification:

[](started(contract.transferFrom(from, to, value), from != address(0) && to != address(0) && from != to && value <= _balances[from] && value <= _allowances[from][msg.sender] && _balances[to] + value < 0x10000000000000000000000000000000000000000000000000000000000000000 && value >= 0 && _balances[to] >= 0 && _balances[from] >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _allowances[from][msg.sender] >= 0 && _allowances[from][msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transferFrom(from, to, value), return == true)))

erc20-transferfrom-succeed-self

Function transferFrom Succeeds on Admissible Self Transfers. All invocations of transferFrom(from, dest, amount) where the dest address equals the from address (i.e. self-transfers) must succeed and return true if:

  • The value of amount does not exceed the balance of address from,
  • the value of amount does not exceed the allowance of msg.sender for address from, and
  • the supplied gas suffices to complete the call. Specification:

[](started(contract.transferFrom(from, to, value), from != address(0) && from == to && value <= _balances[from] && value <= _allowances[from][msg.sender] && value >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _allowances[from][msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transferFrom(from, to, value), return == true)))

erc20-transferfrom-correct-amount

Function transferFrom Transfers the Correct Amount in Non-self Transfers. All invocations of transferFrom(from, dest, amount) that succeed and that return true subtract the value in amount from the balance of address from and add the same value to the balance of address dest. Specification:

[](willSucceed(contract.transferFrom(from, to, value), from != to && value >= 0 && _balances[from] >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[to] >= 0 && _balances[to] + value < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transferFrom(from, to, value), return == true ==> _balances[from] == old(_balances[from]) - value && _balances[to] == old(_balances[to] + value))))

erc20-transferfrom-correct-amount-self

Function transferFrom Performs Self Transfers Correctly. All non-reverting invocations of transferFrom(from, dest, amount) that return true and where the address in from equals the address in dest (i.e. self-transfers) do not change the balance entry of the from address (which equals dest). Specification:

[](willSucceed(contract.transferFrom(from, to, value), from == to && value >= 0 && value < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[from] >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transferFrom(from, to, value), return == true ==> _balances[from] == old(_balances[from]))))

erc20-transferfrom-correct-allowance

Function transferFrom Updated the Allowance Correctly. All non-reverting invocations of transferFrom(from, dest, amount) that return true must decrease the allowance for address msg.sender over address from by the value in amount. Specification:

[](willSucceed(contract.transferFrom(from, to, value), value >= 0 && value < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[from] >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[to] >= 0 && _balances[to] < 0x10000000000000000000000000000000000000000000000000000000000000000 && _allowances[from][msg.sender] >= 0 && _allowances[from][msg.sender] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.transferFrom(from, to, value), return == true ==> ((_allowances[from][msg.sender] == old(_allowances[from][msg.sender]) - value) || (_allowances[from][msg.sender] == old(_allowances[from][msg.sender]) && (from == msg.sender || old(_allowances[from][msg.sender]) == 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF))))))

erc20-transferfrom-change-state

Function transferFrom Has No Unexpected State Changes. All non-reverting invocations of transferFrom(from, dest, amount) that return true may only modify the following state variables:

  • The balance entry for the address in dest,
  • The balance entry for the address in from,
  • The allowance for the address in msg.sender for the address in from. Specification:

[](willSucceed(contract.transferFrom(from, to, amount), p1 != from && p1 != to && (p2 != from || p3 != msg.sender)) ==> <>(finished(contract.transferFrom(from, to, amount), return == true ==> (_totalSupply == old(_totalSupply) && _balances[p1] == old(_balances[p1]) && _allowances[p2][p3] == old(_allowances[p2][p3]) && other_state_variables == old(other_state_variables)))))

erc20-transferfrom-fail-exceed-balance

Function transferFrom Fails if the Requested Amount Exceeds the Available Balance. Any call of the form transferFrom(from, dest, amount) with a value for amount that exceeds the balance of address from must fail. Specification:

[](started(contract.transferFrom(from, to, value), value > _balances[from] && _balances[from] >= 0 && _balances[from] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return == false)))

erc20-transferfrom-fail-exceed-allowance

Function transferFrom Fails if the Requested Amount Exceeds the Available Allowance. Any call of the form transferFrom(from, dest, amount) with a value for amount that exceeds the allowance of address msg.sender must fail. Specification:

[](started(contract.transferFrom(from, to, value), value > _allowances[from][msg.sender] && _allowances[from][msg.sender] >= 0 && value < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(reverted(contract.transferFrom) || finished(contract.transferFrom(from, to, value), return == false) || finished(contract.transferFrom(from, to, value), return == true && (msg.sender == from || _allowances[from][msg.sender] == 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF))))

erc20-transferfrom-fail-recipient-overflow

Function transferFrom Prevents Overflows in the Recipient's Balance. Any call of transferFrom(from, dest, amount) with a value in amount whose transfer would cause an overflow of the balance of address dest must fail. Specification:

[](started(contract.transferFrom(from, to, value), from != to && _balances[to] + value >= 0x10000000000000000000000000000000000000000000000000000000000000000 && value < 0x10000000000000000000000000000000000000000000000000000000000000000 && _balances[to] >= 0 && _balances[to] < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(reverted(contract.transferFrom) || finished(contract.transferFrom(from, to, value), return == false) || finished(contract.transferFrom(from, to, value), _balances[to] > old(_balances[to]) + value - 0x10000000000000000000000000000000000000000000000000000000000000000)))

erc20-transferfrom-false

If Function transferFrom Returns false, the Contract's State Has Not Been Changed. If transferFrom returns false to signal a failure, it must undo all incurred state changes before returning to the caller. Specification:

[](willSucceed(contract.transferFrom(from, to, value)) ==> <>(finished(contract.transferFrom(from, to, value), return == false ==> (_balances == old(_balances) && _totalSupply == old(_totalSupply) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables)))))

erc20-transferfrom-never-return-false

Function transferFrom Never Returns false. The transferFrom function must never return false. Specification:

[](!(finished(contract.transferFrom, return == false)))

Properties related to function totalSupply

erc20-totalsupply-succeed-always

Function totalSupply Always Succeeds. The function totalSupply must always succeeds, assuming that its execution does not run out of gas. Specification:

[](started(contract.totalSupply) ==> <>(finished(contract.totalSupply)))

erc20-totalsupply-correct-value

Function totalSupply Returns the Value of the Corresponding State Variable. The totalSupply function must return the value that is held in the corresponding state variable of contract contract. Specification:

[](willSucceed(contract.totalSupply) ==> <>(finished(contract.totalSupply, return == _totalSupply)))

erc20-totalsupply-change-state

Function totalSupply Does Not Change the Contract's State. The totalSupply function in contract contract must not change any state variables. Specification:

[](willSucceed(contract.totalSupply) ==> <>(finished(contract.totalSupply, _totalSupply == old(_totalSupply) && _balances == old(_balances) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables))))

Properties related to function balanceOf

erc20-balanceof-succeed-always

Function balanceOf Always Succeeds. Function balanceOf must always succeed if it does not run out of gas. Specification:

[](started(contract.balanceOf) ==> <>(finished(contract.balanceOf)))

erc20-balanceof-correct-value

Function balanceOf Returns the Correct Value. Invocations of balanceOf(owner) must return the value that is held in the contract's balance mapping for address owner. Specification:

[](willSucceed(contract.balanceOf) ==> <>(finished(contract.balanceOf(owner), return == _balances[owner])))

erc20-balanceof-change-state

Function balanceOf Does Not Change the Contract's State. Function balanceOf must not change any of the contract's state variables. Specification:

[](willSucceed(contract.balanceOf) ==> <>(finished(contract.balanceOf(owner), _totalSupply == old(_totalSupply) && _balances == old(_balances) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables))))

Properties related to function allowance

erc20-allowance-succeed-always

Function allowance Always Succeeds. Function allowance must always succeed, assuming that its execution does not run out of gas. Specification:

[](started(contract.allowance) ==> <>(finished(contract.allowance)))

erc20-allowance-correct-value

Function allowance Returns Correct Value. Invocations of allowance(owner, spender) must return the allowance that address spender has over tokens held by address owner. Specification:

[](willSucceed(contract.allowance(owner, spender)) ==> <>(finished(contract.allowance(owner, spender), return == _allowances[owner][spender])))

erc20-allowance-change-state

Function allowance Does Not Change the Contract's State. Function allowance must not change any of the contract's state variables. Specification:

[](willSucceed(contract.allowance(owner, spender)) ==> <>(finished(contract.allowance(owner, spender), _totalSupply == old(_totalSupply) && _balances == old(_balances) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables))))

Properties related to function approve

erc20-approve-revert-zero

Function approve Prevents Giving Approvals For the Zero Address. All calls of the form approve(spender, amount) must fail if the address in spender is the zero address. Specification:

[](started(contract.approve(spender, value), spender == address(0)) ==> <>(reverted(contract.approve) || finished(contract.approve(spender, value), return == false)))

erc20-approve-succeed-normal

Function approve Succeeds for Admissible Inputs. All calls of the form approve(spender, amount) must succeed, if

  • the address in spender is not the zero address and
  • the execution does not run out of gas. Specification:

[](started(contract.approve(spender, value), spender != address(0)) ==> <>(finished(contract.approve(spender, value), return == true)))

erc20-approve-correct-amount

Function approve Updates the Approval Mapping Correctly. All non-reverting calls of the form approve(spender, amount) that return true must correctly update the allowance mapping according to the address msg.sender and the values of spender and amount. Specification:

[](willSucceed(contract.approve(spender, value), spender != address(0) && value >= 0 && value < 0x10000000000000000000000000000000000000000000000000000000000000000) ==> <>(finished(contract.approve(spender, value), return == true ==> _allowances[msg.sender][spender] == value)))

erc20-approve-change-state

Function approve Has No Unexpected State Changes. All calls of the form approve(spender, amount) must only update the allowance mapping according to the address msg.sender and the values of spender and amount and incur no other state changes. Specification:

[](willSucceed(contract.approve(spender, value), spender != address(0) && (p1 != msg.sender || p2 != spender)) ==> <>(finished(contract.approve(spender, value), return == true ==> _totalSupply == old(_totalSupply) && _balances == old(_balances) && _allowances[p1][p2] == old(_allowances[p1][p2]) && other_state_variables == old(other_state_variables))))

erc20-approve-false

If Function approve Returns false, the Contract's State Has Not Been Changed. If function approve returns false to signal a failure, it must undo all state changes that it incurred before returning to the caller. Specification:

[](willSucceed(contract.approve(spender, value)) ==> <>(finished(contract.approve(spender, value), return == false ==> (_balances == old(_balances) && _totalSupply == old(_totalSupply) && _allowances == old(_allowances) && other_state_variables == old(other_state_variables)))))

erc20-approve-never-return-false

Function approve Never Returns false. The function approve must never returns false. Specification:

[](!(finished(contract.approve, return == false)))

Comments

All Comments

Recommended for you

  • DMDAO Burns Nearly 35,000 Tokens Over the Past 7 Days, Bringing Total DMD Burned to Over 716,000

    On September 3, 2026, the latest on-chain data monitoring showed that from August 28 to September 3, 2026, the DMDAO distributed market-making protocol ecosystem maintained a high and stable level of activity, with a cumulative 34,928.27 DMD burned over the past 7 days.

  • Trump Shares Op-Ed Claiming He is Winning the War Against Iran

    On August 29, U.S. President Trump shared a commentary article from the New York Post on Truth Social on Saturday, which stated that he is winning the war against Iran and should maintain the current strategy. The title of the article Trump shared read: 'Trump is Winning the War Against Iran - Stay the Course.'

  • Morgan Stanley: 2028 as a Key Observation Point for Global Memory Competition Landscape

    On August 29, Morgan Stanley pointed out that the rise of Chinese memory manufacturers should not be viewed merely as a technological catch-up or low-cost substitution; what is truly noteworthy is that their production capacity may gradually become large enough to alter the supply structure of the global memory market. Changxin Technology and Yangtze Memory Technologies are currently entering the mainstream product market and gradually extending into high-profit markets such as HBM, high-end server DRAM, and enterprise SSDs. Morgan Stanley considers 2028 as an important observation point for the global memory competition landscape. From 2026 to 2027, demand for AI servers, capacity crowding of advanced wafers by HBM, import substitution, and the time required for customer certification may absorb most of the new supply from Chinese memory manufacturers. By 2028, as Chinese manufacturers expand production, the additional capacity from Samsung, SK Hynix, and Micron, which had previously initiated expansions, will also be released. At that time, the supply variables in the global memory market will significantly increase. Morgan Stanley estimates that Changxin's DRAM monthly production capacity will rise from 180,000 wafers in 2025 to 300,000 in 2026, accounting for approximately 13% of global DRAM wafer capacity and about 11% of bit shipments; by 2028, it is expected to further increase to 500,000 wafers, and by 2031, it could reach 800,000 wafers. If the expansion proceeds smoothly, Changxin's global DRAM bit shipment market share could approach 15% by 2030, and it may even have the opportunity to surpass Micron in production capacity around 2028, becoming the third-largest DRAM supplier in the world.

  • US Spot Ethereum ETF Sees Net Inflow of $102.17 Million Yesterday

    On August 29, according to monitoring by Trader T, the US spot Ethereum ETF recorded a net inflow of $102.17 million yesterday.

  • US Spot Ethereum ETF Sees Net Inflow of $102.17 Million

    On August 29, according to monitoring by Trader T, the US spot Ethereum ETF experienced a net inflow of $102.17 million yesterday.

  • US Spot Bitcoin ETF Sees Net Outflow of $201.81 Million

    On August 29, according to monitoring by Trader T, the US spot Bitcoin ETF experienced a net outflow of $201.81 million yesterday.

  • US Spot Bitcoin ETF Sees Net Outflow of $201.81 Million Yesterday

    On August 29, according to monitoring by Trader T, the US spot Bitcoin ETF experienced a net outflow of $201.81 million yesterday.

  • BTC Surpasses $78,000

    Market data shows that BTC has surpassed $78,000, currently priced at $78,009.49. The 24-hour decline has narrowed to 3.23%. Due to significant market fluctuations, please ensure proper risk management.

  • BTC Surpasses $78,000

    Market data shows that BTC has surpassed $78,000, currently priced at $78,009.49, with a 24-hour decline narrowing to 3.23%. The market is experiencing significant volatility, so please ensure proper risk management.

  • BTC Briefly Drops Below $77,000

    Market data shows that BTC briefly fell below $77,000, currently reported at $77,694, with a 24-hour decline of 3.3%. The market is experiencing significant volatility, so please ensure proper risk management.

Daily Must-Read

Popular Activities

RaveDAO at Terra Solis by Tomorrowland: A Female-Led Techno Night Where Web3 Culture Converges

RaveDAO at Terra Solis by Tomorrowland: A Female-Led Techno Night Where Web3 Culture Converges

April 30 - April 30
Dubai

Popular Tags

Cointime
News
Contents
RSS
Company