formal verification

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.

what the verifier proves

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.

per-contract results

advisory notes

the factory, router, helpers and oracle carry advisory notes (zero safety errors). every one is the same shape: an unsigned amount is allowed to be zero. that is intentional, a zero minimum-output means "no slippage floor", a zero maximum on one side is how a single-sided liquidity add works, and a zero protocol fee simply turns that fee off. forcing these to be non-zero would break legitimate use, so the values are left open by design. the pool and the quoter are the two exceptions: they do not pass, and every finding in both is the same signed-integer kind described above. concentrated liquidity cannot be expressed without signed ticks and signed liquidity deltas, so these two are covered by audit and tests instead of by the prover.

the pool

the concentrated-liquidity pool and the quoter are the two contracts 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, while the verifier model requires value-like fields to be unsigned. the quoter now returns a tick as part of its step simulation, so it inherits the same note. both are covered instead by the multi-agent security audit and by live on-chain tests: the pool asks each token whether the money actually arrived before it credits liquidity or a swap, and it stops by itself after four crossed position boundaries because the language allows no deeper recursion. the router calls the pool six times in a row, so one swap crosses about twenty four boundaries. deposits, swaps in both directions, exact-output swaps, fee collection, liquidity removal and a full run of 34 attacks were each executed end-to-end after deploy.

disclaimer

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 the tokens have no real value.