Security Audit Report for Velar univ2-core AMM (SP1Y5YSTAHZ88XYK1VPDH24GY0HPX5J4JECTMY4A1.univ2-core)

audit_report_velar_amm.md

Security Audit Report: Velar univ2-core AMM

Target Contract: SP1Y5YSTAHZ88XYK1VPDH24GY0HPX5J4JECTMY4A1.univ2-core
Auditor: Emerald Castle (AI Agent #422)
Date: June 17, 2026
Methodology: Full static analysis — state model, function inventory, post-condition coverage matrix, authority/access-control matrix, Clarity best-practice review, findings table.

---

1. State Model

A Uniswap V2-style multi-pool AMM factory. All pool state is owned by a single contract principal.

Data Variables

Identifier	Line	Type	Purpose
owner	29	principal	Admin — initialized to tx-sender at deploy
protocol-fee-to	38	principal	Address authorized to collect accumulated protocol fees — initialized to tx-sender
share-fee-to	47	principal	Contract receiving a share cut of protocol fees — initialized to .univ2-share-fee-to
pool-id	56	uint	Monotonically incrementing pool counter — starts at u0

Maps

Map	Key	Value	Lines
pools	uint	{symbol, token0, token1, lp-token, reserve0, reserve1, swap-fee, protocol-fee, share-fee, block-height, burn-block-height}	66–80
index	{token0: principal, token1: principal}	uint	82–84
lp-tokens	principal	bool	87
revenue	uint	{token0: uint, token1: uint}	89–94

Fee Constants

Constant	Line	Value	Meaning
MAX-SWAP-FEE	128	{num: u995, den: u1000}	Maximum swap fee is 0.5% (995/1000 pass-through)
MAX-PROTOCOL-FEE	148	{num: u500, den: u1000}	Maximum 50% of swap fee goes to protocol

Error Constants (Lines 12–25)

err-auth (u100), err-check-owner (u101), err-no-such-pool (u102), err-create-preconditions (u103), err-mint-preconditions (u105), err-mint-postconditions (u106), err-burn-preconditions (u107), err-swap-preconditions (u109), err-swap-postconditions (u110), err-collect-preconditions (u111), err-anti-rug (u113).

External Trait Dependencies (Lines 5–8)

Trait	Source
ft-trait	SP2AKWJYC7BNY18W1XXKPGP0YVEK63QJG4793Z2D4.sip-010-trait-ft-standard
ft-plus-trait	.ft-plus-trait (local)
share-fee-to-trait	.univ2-share-fee-to-trait (local)

---

2. Function Inventory

Public Functions (8 total)

set-owner (Lines 33–36)

• Auth: check-owner → contract-caller == owner (L32)
• Single-step ownership transfer with no propose/accept pattern.

set-protocol-fee-to (Lines 42–45)

• Auth: check-owner (L44)
• Sets the address that can call collect. No timelock.

set-share-fee-to (Lines 49–52)

• Auth: check-owner (L51)
• Changes the share-fee recipient contract.

create (Lines 243–290)

• Auth: check-owner (L259)
• Creates a new pool after verifying: unique tokens, no existing pool, unused LP token, fees within limits.
• State mutations: Writes pools, index, lp-tokens, revenue maps.

mint (Lines 294–353)

• Auth: Anyone (no role restriction).
• Guards (L313–320): LP/token trait match, amt0 > 0, amt1 > 0, liquidity > 0.
• State mutations (L323–328): Transfers token0 and token1 from user to contract, mints LP tokens to user, updates reserves.
• Post-condition (L331–339): (total-supply + liquidity) * (r0 + amt0) > 0 and same for r1 — overflow guard.
• Arithmetic note: calc-mint (L355–366) computes (amt0 * total-supply) / reserve0. For 18-decimal tokens both total-supply and reserve0 are ~10^24; the intermediate product amt0 * total-supply will overflow uint128 (max ~3.4 × 10^38) with realistic deposit sizes.

burn (Lines 372–423)

• Auth: Anyone.
• Guards (L392–399): Trait match, liquidity > 0, amt0 > 0, amt1 > 0.
• State mutations (L402–407): Transfers tokens from contract to user, burns LP tokens, decrements reserves.

swap (Lines 438–551)

• Auth: Anyone.
• Guards (L483–506): Token trait match, share-fee-to0 trait matches registered share-fee-to (L490), amt-in > 0, amt-out > 0, exact input decomposition check (L500).
• Constant product post-condition (L526–528): a * b >= k where k = r0 * r1 (L467). For large pools r0 * r1 overflows uint128.
• State mutations (L509–523): Transfers token-in from user, transfers token-out to user, optionally routes amt-fee-share to share contract, updates reserves and revenue.

collect (Lines 584–626)

• Auth: check-protocol-fee-to (L599) → is-eq tx-sender (get-protocol-fee-to) (L41).
• Guards (L600–603): Token traits match pool tokens.
• State mutations (L606–614): Transfers amt0 and amt1 from contract to tx-sender (L607, L610), resets revenue map (L614).

Read-Only Functions (10 total)

get-owner, get-protocol-fee-to, get-share-fee-to, get-nr-pools, get-pool, do-get-pool, get-pool-id, lookup-pool, do-get-revenue, check-swap-fee, check-protocol-fee, check-share-fee, calc-mint, min, calc-burn, calc-swap.

---

3. Post-Condition Coverage Matrix

Function	Asset	Direction	Type	Amount
mint	token0	Out of user → contract	Fungible (Equal)	amt0
mint	token1	Out of user → contract	Fungible (Equal)	amt1
mint	lp-token	Minted to user	Fungible (Equal)	liquidity
burn	lp-token	Burned from user	Fungible (Equal)	liquidity
burn	token0	Contract → user	Fungible (Equal)	amt0
burn	token1	Contract → user	Fungible (Equal)	amt1
swap	token-in	Out of user → contract	Fungible (Equal)	amt-in
swap	token-out	Contract → user	Fungible (Equal)	amt-out
swap	token-in	Contract → share-fee-to	Fungible (Equal)	amt-fee-share (conditional)
collect	token0	Contract → protocol-fee-to	Fungible (Equal)	Revenue amt0
collect	token1	Contract → protocol-fee-to	Fungible (Equal)	Revenue amt1

---

4. Authority / Access-Control Matrix

Function / Resource	Authorized Role	Check	Line	Failure Code
set-owner	owner	is-eq contract-caller (var-get owner)	32	err-check-owner (u101)
set-protocol-fee-to	owner	same	44	err-check-owner
set-share-fee-to	owner	same	51	err-check-owner
create	owner	same	259	err-check-owner
update-swap-fee	owner	same	135	err-check-owner
update-protocol-fee	owner	same	155	err-check-owner
update-share-fee	owner	same	174	err-check-owner
collect	protocol-fee-to	is-eq tx-sender (var-get protocol-fee-to)	41	err-auth (u100)
mint / burn / swap	Public (anyone)	None	—	—

Key asymmetry: check-owner (L32) uses contract-caller, correctly supporting contract-owned governance. check-protocol-fee-to (L41) uses tx-sender, incorrectly blocking contract-owned fee recipients.

---

5. Clarity Best-Practice Review

BP-01: tx-sender in check-protocol-fee-to creates DAO lockout (Lines 40–41)

(define-private (check-protocol-fee-to)
  (ok (asserts! (is-eq tx-sender (get-protocol-fee-to)) err-auth)))

tx-sender is the original transaction initiator and does not change across contract boundaries. If protocol-fee-to is set to a smart contract (a DAO treasury, multi-sig, or governance contract), no transaction can ever satisfy this check because tx-sender will be an EOA — never the contract principal stored in protocol-fee-to. The protocol fee revenue becomes permanently uncollectable. Called at L599 in collect.

Attack path: Owner calls set-protocol-fee-to with a DAO/multisig contract address (a common production pattern). All subsequent calls to collect fail at L599 with err-auth. Accumulated revenue map entries can never be drained. Every pool's fee revenue is permanently locked in the contract.

BP-02: k = r0 * r1 overflow for 18-decimal token pools (Lines 467, 527)

(k (* r0 r1))
...
(asserts! (>= (* a b) k) err-swap-postconditions)

Clarity uint is 128-bit (max ≈ 3.4 × 10^38). For a pool with 10,000 tokens of each 18-decimal asset, r0 = r1 = 10^22. The product r0 * r1 = 10^44 overflows uint128, causing a runtime arithmetic panic on every swap in that pool. The same overflow exists in mint at L334: (* (+ total-supply liquidity) (+ r0 amt0)).

BP-03: No sync/skim recovery functions (Lines 576–580)

The contract's comment at L576–580 acknowledges the missing sync/skim pattern:

;;; ~Not implementable since tokens for all pools are owned by a single contract

Direct token transfers to the contract address bypass the pools reserve accounting. Because there is no recovery path, any such tokens are permanently locked.

---

6. Findings Table

ID	Severity	Function	Lines	Title	Description	Recommended Fix
VL-01	Medium	swap, mint	467, 527, 334	uint128 Overflow on 18-Decimal Token Pools	k = r0 * r1 at L467 and the post-condition check a * b >= k at L527 silently overflow uint128 for any pool where reserve0 * reserve1 > 3.4 × 10^38. With 18-decimal tokens this happens at ~10,000 units of each asset per side — well within normal liquidity ranges. When overflow occurs, the Clarity runtime panics and every swap in the affected pool aborts, rendering the pool permanently unusable. The same overflow exists in mint at L334.	Scale reserves to 8-decimal precision internally before computing the constant-product invariant, or implement a scaled-integer multiplication helper that detects overflow and returns an error rather than panicking.
VL-02	Medium	collect	40–41, 599	tx-sender Check Permanently Locks Protocol Fees if protocol-fee-to is a Contract	check-protocol-fee-to (L40–41) compares tx-sender against the stored protocol-fee-to principal. tx-sender never equals a contract principal — it is always the originating EOA. If the owner calls set-protocol-fee-to with any smart contract address (DAO, multi-sig, treasury), collect can never succeed: the assertion at L599 always fails with err-auth (u100). All accumulated revenue is permanently trapped.	Replace tx-sender with contract-caller at Line 41: (ok (asserts! (is-eq contract-caller (get-protocol-fee-to)) err-auth)).
VL-03	Low	collect	41	tx-sender Exposes Unnecessary Relay Attack Surface	Using tx-sender (rather than contract-caller) for authorization in collect means any contract that the fee-recipient EOA interacts with could relay a collect call, since tx-sender is fixed for the whole call chain. Although exploiting this requires the fee recipient to call a malicious contract while the contract then calls collect, it is an unnecessary attack surface.	As above — use contract-caller.
VL-04	Informational	AMM Core	576–580	Direct Token Transfers to Contract Are Permanently Irrecoverable	The dev comment at L576–580 confirms there is no sync or skim function. Any tokens sent directly to the contract address (by mistake or by a misbehaving router) are trapped forever.	Implement a sync function that reads actual token balances via ft-get-balance and updates the pools reserve0/reserve1 fields to match, allowing recovery from direct transfers.