Home

Awesome

Security Audits by Informal Systems

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.

Public Audit Reports

Audit date(s)ClientAudit report
2023-11-11NeutronNeutron: Duality v0.5.0 + integration of Cosmos SDK 0.47
2023-11-05NeutronNeutron: Overrule + Liquidity Migration Smart Contracts
2023-09-13CelestiaCelestia: rsmt2d library
2023-06-23OsmosisOsmosis: Concentrated Liquidity module
2023-05-16DualityDuality: Dex and Incentives modules
2023-04-11SkipSkip: mev-tendermint
2023-04-06NeutronNeutron: Neutron-SDK, DAO, Wasmd, TGE contracts
2023-03-27CelestiaCelestia: Namespaced Merkle Tree
2023-03-27OsmosisOsmosis: Crosschainswaps and Swaprouter modules
2023-03-27OsmosisOsmosis: Token Transfer Analysis Testing
2023-02-10Cosmos HubInterchain Security v.1.0: Provider Chain Safety
2022 -- 2023AnomaAnoma Audit Partnership: Proof of Stake
2022-12-25CelestiaCelestia: Payment Module
2022-12-20OsmosisOsmosis: TWAP and GAMM modules
2022-11-30StrideStride: StakeIBC and ICACallbacks Modules
2022-09-30OsmosisOsmosis: Token Factory
2023-02-03Delphi LabsMars Protocol: Envoy module
2022-02-02AgoricAgoric: Swingset Kernel, Comms, and Userspace, Phase 3
2021-11 -- 2021-12EvmosEvmos: Intrarelayer, Staking, and EVM modules
2021-10-21AgoricAgoric: Swingset Kernel and Userspace, Phase 2
2021-09-09InterlayInterBTC: Parachain Modules and Vault Client
2021-07-08AgoricAgoric: Swingset Kernel and Userspace, Phase 1
2021-06-15InjectiveInjective Protocol: Protocol Design
2021-06-12InterlayInterBTC: Parachain
2021-01-25IBC ProtocolIBC: Interblockchain Communication Protocol Specification and Code