factory
factory
formal verification
beyond the adversarial audit, every factory contract is run through octra's formal verifier, a machine-checked value-safety model (backed by a coq proof) that mathematically rules out whole classes of bugs: signed values leaking into balances, unchecked overflow, and unproven supply conservation. the result for each contract is recorded on-chain next to its source, so anyone can read the proof for themselves on the explorer.
a clean formal result is a strong machine-checked guarantee, but it is not a substitute for the security audit or a human review. the two are complementary: the verifier proves the absence of certain bug classes; the audit reasons about economic logic and intent.
the model treats every balance and amount as a value that must stay non-negative and conserved. it rejects a contract that stores a signed number where a value belongs, that adds or subtracts without an overflow/underflow guard, or that moves tokens without proving total supply is preserved. a contract marked safe carries a machine-checked proof that none of these can happen.
| contract | role | address | result |
|---|---|---|---|
| WOCT | wrapped OCT token | oct7Nt4…tY95 ↗ | safe ✓ |
| FACT | protocol token | octCNJq…bR4T ↗ | safe ✓ |
| quoter | swap price quoter | oct8PHL…Qo8n ↗ | safe ✓ |
| stake vault | relayer staking | oct3AuK…w2z6 ↗ | safe ✓ |
| slash escrow | relayer job anchor | oct3vnC…CDkF ↗ | safe ✓ |
| slash multisig | watchtower committee | octEW8d…Pzzg ↗ | safe ✓ |
| factory | pool registry | octGmgc…yZKM ↗ | safe · advisory set_pool_fee_protocol accepts new_fee = 0, which simply turns the protocol fee off (intentional). |
| router | swap router | octGt3G…yJaC ↗ | safe · advisory add_liquidity amount0_max / amount1_max and exact_input_single amount_out_minimum may be 0 (single-sided add and no slippage floor, intentional). |
| swap helper | token→OCT helper | octGHsM…CTzz ↗ | safe · advisory swap_to_native amount_out_minimum may be 0 (no slippage floor, intentional). |
| multihop | atomic 2-hop helper | octHQwK…yj8t ↗ | safe · advisory exact_input_double amount_out_minimum may be 0 (no slippage floor on the route, intentional). |
| SFACT | private-swap stealth wrapper | oct2bWQ…Beo5 ↗ | safe · advisory stealth_claim output_id and the get_output_payload / get_output_claimed id may be 0; supply conservation is not proven for stealth_transfer / stealth_claim (inherent to the one-time-output stealth model). |
| pool | concentrated-liquidity pool | oct4gRg…YrXb ↗ | audit + tests |
the router, factory and helpers carry advisory notes (zero safety errors). each is the same shape: a minimum-output or maximum-spend amount is allowed to be zero. that is intentional, a zero minimum-output means "no slippage floor", and a zero maximum on one side is how a single-sided liquidity add works. forcing these to be non-zero would break legitimate use, so the values are left open by design. SFACT's notes are inherent to the stealth/inbox model, where balances move into one-time outputs rather than a single conserved ledger.
the concentrated-liquidity pool is the one contract the value-safety model cannot express. uniswap-v3-style liquidity needs signed quantities by construction, ticks run from −887272 to +887272 and liquidity deltas are signed, and the verifier's model requires value-like fields to be unsigned. so the pool cannot be marked "safe" by this tool. it is instead covered by the multi-agent security audit and by live on-chain tests: the critical fixes (unauthorized burn, stale fee growth, price runaway past liquidity) were reproduced and re-verified against the deployed pool, and swaps, fee collection and liquidity removal were each run end-to-end after deploy.
every result here is reproducible: read a contract's stored source with contract_source(address) or re-run the check with octra_compileAml(source) against the same devnet RPC.
formal verification proves the properties its model captures; it does not prove the contract does what you expect, and it does not cover the pool's economic math, the underlying octra chain, or third-party wallets. factory is beta software on devnet, where all tokens come from the faucet and have no real value.