We prove our code twice: Certora + TLA+ formal verification at Token-x
Most platforms test their smart contracts. We prove them. Here's what that means for the safety of your assets — and why we verify at two separate levels.
When a bank holds your money, you rely on decades of regulation, audits, and legal backstops. When a tokenization platform holds your assets on-chain, you rely on the code. The question worth asking before committing capital: how do you know the code is correct?
Most teams answer this with testing: write scenarios, run them, ship if they pass. Testing is necessary. It is not sufficient. A test can only check the inputs you thought to try. Formal verification checks all possible inputs — every account balance, every sequence of transactions, every interleaving of concurrent operations — mathematically.
Token-x verifies its critical code at two independent levels, using two tools that have different blind spots. A flaw that slips past one is almost certain to be caught by the other.
What formal verification actually means
A software test asks: "does this specific input produce the right output?" A formal proof asks: "for every possible input, is this property true?" The difference is not incremental — it is the difference between sampling a lake and proving the water is safe.
For a security token platform, the properties that matter most are: can tokens be transferred to an unwhitelisted investor? Can a compliance lockup be bypassed? Can the same trade settle twice? Can a vesting grant be partially lost? These are not edge cases to test — they are invariants to prove.
Layer 1: Certora — proving smart contract bytecode
The Certora Prover takes compiled Solidity bytecode and converts it into a mathematical model. It then exhaustively checks every rule and invariant you specify — across all possible callers, all possible balances, all possible states the contract can reach. No fuzzer, no matter how sophisticated, covers this space.
We run Certora specs on four contracts that sit at the core of every token transaction on Token-x:
| Contract | What we proved |
|---|---|
| VestingVault | Token conservation on revoke: vested + unvested always equals the original grant. No tokens can be permanently locked in the vault under any execution sequence. |
| ATSSettlement | No fill can settle twice. Payment amount must exactly equal qty × price normalised to the payment token's decimal precision — the contract rejects any caller-supplied amount that doesn't match. |
| TimeLockModule | An investor under a Reg D lockup cannot transfer tokens regardless of amount, recipient, or caller. After lock expiry, transfers are unconditionally permitted. |
| TokenXToken | Frozen addresses cannot send or receive. Partial freezes enforce the exact available balance. Total supply changes only via mint and burn — never by transfer. |
The Certora specs are checked against the actual deployed bytecode, not the source. A compiler bug that changed the semantics of the Solidity would be caught here.
During specification, we discovered a real bug: the original VestingVault.revoke() did not transfer vested-but-unreleased tokens to the beneficiary before sealing the schedule — those tokens would have been permanently locked. The Certora token conservation rule made the flaw impossible to miss. The fix was deployed before mainnet.
Layer 2: TLA+ — proving distributed system protocols
Smart contract verification covers what happens inside a single contract. It cannot reason about what happens across the API service, the blockchain connector, the order matcher, and the Temporal workflow engine — all running concurrently, all communicating asynchronously.
TLA+ is a specification language for concurrent and distributed systems. Its model checker (TLC) exhaustively explores every possible interleaving of actions across every component. If there is a state reachable through any sequence of operations that violates a safety invariant, TLC finds it and produces the exact execution trace.
We wrote five TLA+ modules covering the coordination protocols unique to a tokenization platform:
Token lifecycle state machine
The 9-step lifecycle from payment through minting through redemption is modelled as a formal state machine. TLC verified that a burn cannot happen without Transfer Agent approval in any possible execution, that the minting lock prevents two concurrent goroutines from double-minting the same subscription, and that every in-progress redemption eventually completes or fails — it cannot become stuck.
Nonce sequencing
Every transaction submitted to an EVM chain requires a unique, sequential nonce. The model explores all interleavings of concurrent transaction submissions and proves no two transactions are ever assigned the same nonce — the condition that causes one transaction to be silently dropped by the chain.
ATS settlement delivery
The Rust order matcher delivers fills to the settlement worker over Redis pub/sub — an at-least-once channel. The model proves that even with unlimited message redeliveries, an idempotency key written before the chain submission prevents any fill from settling twice on-chain.
Chain event idempotency
After a service restart, the chain listener re-scans from the last saved cursor and may replay events already processed. The model proves each business effect — cap table update, subscription status change — is applied exactly once, regardless of how many times the triggering event is delivered.
Cross-chain consistency
Token-x supports 11 blockchain networks. When a token is bridged from one chain to another, the model proves tokens cannot be created from nothing — every mint on a destination chain is preceded by a lock on the source chain, and the database view of balances never exceeds the actual on-chain state.
What this means for your investment
Formal verification does not replace audits — it sharpens them. When a third-party audit firm reviews Token-x's contracts, they are not starting from scratch. The Certora and TLA+ specs give auditors a precise, machine-checked statement of what each component is supposed to do. Their job becomes: verify the specification matches the intent, and find anything the specifications don't cover.
- Your tokens cannot be transferred to an unverified wallet — the whitelist check is in the EVM and formally proved.
- Regulation D 12-month lockups are enforced at the contract level, not in application middleware that can be misconfigured.
- Vesting grants are mathematically conserved — no implementation defect can permanently lock your allocation.
- Settlement is idempotent — a system failure during trade confirmation cannot cause your payment to be debited twice.
What we don't claim
Formal verification proves correctness relative to a specification. If the specification is wrong — if we modelled the wrong property — the proof is still valid but the contract may behave unexpectedly. This is why the audit step matters: a human reviewer reads the specification against the legal and regulatory intent, not just the code.
We also do not claim the off-chain components — the API, the frontend, the KYC provider — are formally verified. They are covered by integration tests, chaos tests under simulated failure, and audit trail requirements. Formal verification is applied where the stakes are highest and the failure modes are most severe: the smart contracts that hold your assets and the distributed protocols that coordinate the transfer of value.
The full specification files are available to institutional due diligence reviewers under NDA. Contact us at hello@token-x.finance to request access.