Informal Systems apply a multi-layered, automated approach to our security
audits for the blockchain ecosystem. Under the guidance of leading researchers
in protocol design, verification, and testing, we leverage
our formal verification techniques and tools -- including Quint specification language, Apalache model checker, or Atomkraft E2E testing tool -- to make distributed
systems secure and resilient.
You may read more about our approach at the
Security Services page.
| Audit date(s) | Client | Audit report | Announcement |
|---|
| 2026 | Zenrock | Zenrock Q1 2026 - Hush Privacy Protocol | |
| 2025 | Anoma | Anoma Q4 2025: RISC Zero RM & EVM Protocol Adapter | |
| 2025 | Anoma | Anoma Q2 2025: E2E Shielded Transaction & Balance Consistency | |
| 2025 | Neutron | Neutron Q3 2025: DEX Fractional | |
| 2025 | Neutron | Neutron/Timewave Q3 2025: Valence Protocol | |
| 2025 | Celestia | Celestia Q2 2025: High-Throughput Recovery Audit | |
| 2025 | Espresso | Espresso Q1 2025: Epoch Change Protocol | |
| 2025 | Apex | Apex Q1 2025: Reactor and Skyline critical path | |
| 2025 | Celestia | Celestia Q2 2025: CIP 31 | |
| 2025 | Left Curve | Jellyfish Merkle Tree Specification | Finding |
| 2025 | Ripple | XRPL EVM Sidechain | Blog post by Ajit Kulkarni (Ripple) |
| 2024 | DYDX | DYDX: Vaults | |
| 2024 | DYDX | DYDX: Q2 Audit | |
| 2024 | DYDX | DYDX: Q1 Audit | |
| 2023 | DYDX | DYDX: Q4 Audit | Blog Post by dYdX |
| 2024 | Neutron | Neutron: Dex Model | |
| 2024 | Anoma | Namada: Governance and Public Goods Funding | |
| 2024 | Anoma | Namada: IBC & MASP Integrations | |
| 2024 | Anoma | Namada: Namada ABCI, Replay Protection, Fee and Gas Metering | |
| 2024 | Anoma | Namada: Masp | Blog Post by Namada |
| 2023 | Neutron | Neutron: Duality v0.5.0 + integration of Cosmos SDK 0.47 | Blog Post by Neutron |
| 2023 | Neutron | Neutron: Overrule + Liquidity Migration Smart Contracts | |
| 2023 | Celestia | Celestia: rsmt2d library | |
| 2023 | Osmosis | Osmosis: Concentrated Liquidity module | |
| 2023 | Duality | Duality: Dex and Incentives modules | |
| 2023 | Skip | Skip: mev-tendermint | |
| 2023 | Neutron | Neutron: Neutron-SDK, DAO, Wasmd, TGE contracts | |
| 2023 | Celestia | Celestia: Namespaced Merkle Tree | |
| 2023 | Osmosis | Osmosis: Crosschainswaps and Swaprouter modules | |
| 2023 | Osmosis | Osmosis: Token Transfer Analysis Testing | |
| 2023 | Cosmos Hub | Interchain Security v.1.0: Provider Chain Safety | |
| 2023 | Anoma | Anoma Audit Partnership: Proof of Stake | |
| 2022 | Celestia | Celestia: Payment Module | |
| 2022 | Osmosis | Osmosis: TWAP and GAMM modules | |
| 2022 | Stride | Stride: StakeIBC and ICACallbacks Modules | |
| 2022 | Osmosis | Osmosis: Token Factory | |
| 2023 | Delphi Labs | Mars Protocol: Envoy module | |
| 2022 | Agoric | Agoric: Swingset Kernel, Comms, and Userspace, Phase 3 | |
| 2021 | Evmos | Evmos: Intrarelayer, Staking, and EVM modules | |
| 2021 | Agoric | Agoric: Swingset Kernel and Userspace, Phase 2 | |
| 2021 | Interlay | InterBTC: Parachain Modules and Vault Client | Blog Post by Gregory Hill (Interlay) |
| 2021 | Agoric | Agoric: Swingset Kernel and Userspace, Phase 1 | |
| 2021 | Injective | Injective Protocol: Protocol Design | Blog Post by Injective |
| 2021 | Interlay | InterBTC: Parachain | |
| 2021 | DYDX | DYDX: Phase III | Blog Post by dYdX |
| 2021 | DYDX | DYDX: Phase I & II | Blog Post by dYdX |
| 2021 | IBC Protocol | IBC: Interblockchain Communication Protocol Specification and Code | |