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

  • Nasdaq Composite Index Surpasses June High, Sets New Record

    On September 22, the Nasdaq Composite Index expanded its early gains to 0.34%, reaching a new record high of 27,214.65 points.

  • Trump Expresses Desire to Meet Iranian Officials in New York if 'Conditions are Right'

    On September 22, CNN reported that U.S. President Trump has told his advisors that he hopes to meet with Iranian officials in New York if 'conditions are right.' The official stated that this meeting could also involve some of Trump's senior advisors who are accompanying him in New York, although no meetings have been scheduled yet. The official also mentioned that it is currently unclear whether Iran is willing to hold a potential meeting. Both Secretary of State Rubio and U.S. Ambassador to the United Nations Thomas-Greenfield have indicated that Trump is 'open' to meeting with Iranian officials.

  • Central Bank Reiterates: No Participation in Virtual Currency Activities

    On September 22, the People's Bank of China released financial education promotional content, reiterating the risks associated with virtual currencies. The central bank clarified that virtual currencies such as Bitcoin, Ethereum, and Tether are not legal tender, do not possess legal compensation, and cannot circulate in the market. Engaging in virtual currency-related businesses within the country is considered illegal financial activity and will be banned by law; foreign institutions are prohibited from illegally providing virtual currency services to domestic entities, and without permission, they cannot issue stablecoins pegged to the Renminbi abroad. The central bank advises the public to be cautious of virtual currency projects that claim high returns and guaranteed profits; do not participate in virtual currency trading, mining, or investment; refrain from joining cryptocurrency trading groups or visiting foreign trading platforms; do not lend bank cards or payment accounts, and refuse to act as currency dealers, U dealers, or fund runners. Any discovery of related illegal activities can be reported to regulatory authorities.

  • Kalshi Requests CFTC Approval for Margin Trading on Its Platform

    On September 22, event prediction platform Kalshi requested the U.S. Commodity Futures Trading Commission (CFTC) to allow margin trading on its platform.

  • CME to Launch BCH and Uniswap Futures to Expand Crypto Derivatives Portfolio

    On September 22, according to market news, the CME will launch BCH (Bitcoin Cash) and Uniswap futures to expand its crypto derivatives portfolio.

  • Binance Acquires $100 Million in Circle Shares at a Discount

    On September 22, Circle (CRCL) filed an 8-K document indicating that its subsidiary entered into a new five-year cooperation agreement with Binance on September 17 to expand the promotion of USDC, replacing previous agreements signed in November 2024 and August 2025. Circle will pay Binance monthly incentive fees based on the amount of USDC held through its modular smart contract wallet infrastructure services. On the same day, Binance subscribed to 1,237,011 shares of Class A common stock of Circle at a discounted price of $80.84 per share, totaling $100 million, with the transaction completed. The related shares are generally subject to a two-year transfer restriction, but there are provisions for early termination and other exceptions.

  • BTC Surpasses $86,000

    Market data shows that BTC has surpassed $86,000, currently priced at $86,009.97, with a 24-hour increase of 2.57%. The market is experiencing significant volatility, so please ensure proper risk management.

  • Spot Gold Falls Below $4,300

    On September 22, spot gold fell below $4,300 per ounce, with a daily decline of 1.00%. New York futures gold also dropped over 1.00% during the day, currently reported at $4,340.00 per ounce.

  • Bitcoin Leads Cryptocurrency Market Value Back Above $3 Trillion

    On September 22, following a remarkable rebound in Bitcoin, the market value of digital assets returned to over $3 trillion for the first time since January. However, traders have flocked to leverage trading in perpetual futures, increasing the risk of rapid price fluctuations. According to CoinGecko data, the cryptocurrency market value has increased by over $740 billion since the U.S. Treasury announced last month that it would increase the repurchase of long-term bonds. Leverage bets have also surged. Coinglass data shows that the open interest in various token perpetual futures has risen to nearly $160 billion, the highest level since late October of last year.

  • First Tokenized Stock Trading Venues May Emerge Next Quarter

    On September 22, Taylor Lindman, Chief Legal Counsel of the SEC's Crypto Special Working Group, stated in an interview that under the SEC's five-year "Innovation Exemption" framework, the first compliant tokenized stock trading venues could gradually take shape as early as next quarter. This exemption has officially come into effect, allowing qualified platforms to conduct tokenized trading of U.S. stocks on public blockchains through licensed automated market makers (AMMs) and liquidity pools. Institutions planning to enter this space are required to issue operational notices and report to the SEC within one business day after publication. These public notices will also serve as important signals for the market to assess which companies are entering this sector. Lindman anticipates that there will be some delay in companies submitting relevant notices, likely falling within the next quarter. SEC Commissioner Hester Peirce and Lindman both emphasized that this model "leans more towards on-chain finance rather than true DeFi," as each trading platform has a clear operating entity responsible for compliance, rather than being completely decentralized peer-to-peer finance.

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