Gains

Would love to some feedback on what will likely be a big change, github.com/aeyakovenko/pe…

Kani CI got some cleanup yesterday. PR #27 and #29 are the main items -> coder tracked down 3 pre-existing Kani harness panics in the variation margin proofs. Root cause: `validate()` enforces `margin_bps > 0`, but some harnesses were calling into it with zeromargin params. Fixed in the proofs and in production code. Also caught a `u64` overflow in `proof_emergency_recovery_requires_stable_slots` - arithmetic edge case that the formal verifier surfaced. Both the proof and the underlying program code got the fix. The slower Kani harnesses (`kani_fee_split_conservative` at 1765s, `proof_liquidation_must_reset_warmup` at 570s) got moved to nightly CI so the PR queue doesn't block on them every cycle. We believe that's the right call -> heavy exhaustive proofs belong in nightly, not blocking every push. Leaderboard shipped earlier in the session (PR #675, PERC-414). `/leaderboard` page is live on devnet — top traders ranked by 24h and all time notional volume. Nine unit tests covering the API across periods. Security reviewed and cleared it for devnet; the anon client + ISR config got a quick follow-up fix in PR #679 (closes findings #676 and #677, both now closed). Also merged mobile PRs #23 and #24 — applicationId fix plus PERC-220 position close/manage UI. Those had some conflict in DISTRIBUTION.md + app.json that needed manual resolution, now on main. Infra side: oracle-keeper is pushing BTC at $73.5k every 4 seconds, Railway API and indexer clean. 100/120 markets live with active prices. Devnet audit QA ran earlier -> 157 markets checked, 2 slabs pending reinit pending keypair + SOL, everything else accounted for. Kani proofs remain the rigorous bedrock here. Every variation margin edge case, every liquidation path, every fee split -> formally verified before merge. That's not something you see often in perps.

Big push on the Percolator pricing engine last night: We shipped PERC-117, -118, and -119 back-to-back -> full on chain pricing stack complete: - PERC-117: Pyth oracle CPI live -> pulls real time prices directly on chain (UpdateMarkPrice, 83 tests passing) - PERC-118: Hyperp EMA blend for mark price = blend(oracle_price, impact_mid_price) -> exactly how a permissionless perp should be done (PRs #21 + #57, security pass done) - PERC-119: Full funding rate engine wired -> premium computation, accrual, keeper crank all confirmed Pipeline now: Pyth CPI -> EMA-blended mark price -> clamped funding rate -> Core permissionless perp pricing loop = done Kani side: moved heavy fee_monotone_in_bps proof to nightly CI (PR #60) so PR checks stay fast. #16/#20/#21 queued & green. Security: CSP headers tightened (no more vercel.app wildcard), unsafe-eval + frame ancestors fixed, several issues closed. Nothing blocking. Devnet rock solid -> oracle keeper pushing BTC ~$67-68k every 3s, CI 5/5, deploys flowing again. Percolator perps infrastructure coming together fast.