Frontier models can now read formal specs. Publish ours, and every attacker starts from our analysis instead of from the code. So we keep them private. The code stays on-chain for anyone to audit; protocol teams we work with see everything. @SuiDevelopers fly safe!

Rust-Prover, our verifier for Rust, proved all 1325 theorems of VeriContest's 1007 problems. Rust-Prover is based on Aeneas (thanks @sonmarcho and the @MSFTResearch team for the amazing work), uses @leanprover as a backend, Opus 5.5 for writing the proofs. This is the the first full solve of the benchmark that we know of. Median 3.4 minutes and $1.20 per proof, each proof checked by Lean's kernel.

Software assurance, including security, is hard to measure or brag about. You do a good job when nobody hears about it. These are the lending protocols on @SuiNetwork that we have formally verified: @Scallop_io @CurrentSUI @navi_protocol Beyond our technical results, we learned that they have solid teams who care about security.

Just read this post by the Sui security team, and fully agree. We've been applying these principles with our partners for a while now: 1. Rule out problems before production -- Move is great here; on the smart-contract layer, our partners' releases are gated by our FV+audit 2. Keep review evidence with the code -- package versions, code, and our FV+audit findings are connected as (package, commit, findings) triples 3. Keep watching after deployment -- both mainnet and github are continuously monitored; whenever the team changes code, our platform automatically updates the FV and surfaces any problems 4. Put attention where the consequences are greatest -- a lot can be done here; for now, our agentic FV+audit infra has deep work prioritization built-in; a run is not a yes/no binary, effort scales with the risk profile of the protocol Looking forward to more of this reporting moving on-chain (attestations) and surfaced in MVR

Comprehensive Formal Verification of the @CetusProtocol DLMM We formally verified the core protocol and the router strategies built on it: swaps, positions, the math kernel, and the bin grid itself. Together with the CLMM verification we published in March, both of Cetus's AMMs are now comprehensively formally verified. @suidevelopers, check it out!

Some of what we proved (the report has the full picture): → Swap conservation: each flash-swap repay credits exactly the receipt's pay amount to the input-side reserve, and every other pool field is proven byte-identical to its pre-call value → Math kernel: swap-amount conversion, liquidity↔amount, fees, and growth accumulators proven against exact integer formulas, down to the floor/ceil rounding direction of each step → Volatility fees: the three-regime time-decay of the volatility references and the quadratic variable-fee formula proven with explicit overflow guards → Access control: seven ACL roles partition the admin surface; covered entry points proven to abort unless the caller holds the role bit and the protocol version is current