Category: blockchain security and protocol-engineering firm / formal-verification audit infrastructure / cross-chain and distributed-systems assurance tooling
Summary: Informal Systems is best cataloged as formal-verification and protocol-assurance infrastructure rather than as a generic audit boutique or a simple Cosmos dev shop. In this pass, the clearest first-party evidence came from the public audits repository, the Quint audit-services page, and the Model Based Techniques documentation. Together those materials describe a team that audits blockchain and distributed systems with model-based methods, publishes a substantial public corpus of reports, and develops its own verification and testing tools such as Quint, Apalache, Modelator, and cosmwasm-to-quint. The key distinction is that Informal is packaging behavioral modeling, verification, testing, and reusable tooling into an ongoing assurance stack instead of only delivering one-off manual code reviews.
What it does:
Performs security audits for blockchain and distributed systems using a formal-verification-heavy approach rather than only manual code review
Publishes a large public audit-report corpus spanning projects such as IBC, dYdX, Celestia, Neutron, Namada, Osmosis, Zenrock, and others
Develops and maintains verification and testing tools including Quint, Apalache, Modelator, and cosmwasm-to-quint
Positions its audit offering around system behavior, formal specification, model-based testing, and production-trace validation
Delivers verification harnesses intended to plug into CI so assurance can continue after the initial audit engagement
Frames the broader company mission around building trustworthy, secure, interoperable, and fault-tolerant software and monetary systems
Key claims:
The public audits repository says Informal applies a multi-layered, automated approach to security audits for the blockchain ecosystem under researchers in protocol design, verification, and testing
The same repository says Informal uses tools such as Quint, Apalache, and Atomkraft to make distributed systems secure and resilient
The Quint audit-services page says the firm audits system behavior, not just code, by modeling intended behavior, verifying properties across possible states, and comparing those properties against implementation and real-world execution
The same page says customers get a verification harness that can plug into CI so every code change is checked against critical security properties, which strongly suggests a continuous-assurance posture rather than a point-in-time report business
The Model Based Techniques page says Informal uses model-based techniques in both its own development practice and its security audit services
That page also lists Quint, Apalache, Modelator, and cosmwasm-to-quint as first-party tools that make model-based techniques easier to incorporate into development and auditing
The Model Based Techniques page says Informal was founded to build trust in software and monetary systems and specializes in secure, interoperable, and fault-tolerant networks
The audits repository shows public reports across several years and ecosystems, including IBC, Celestia, Neutron, Osmosis, Namada, dYdX, Ripple’s XRPL EVM sidechain, and others, reinforcing that Informal operates a reusable assurance practice rather than only a narrow single-chain consultancy
Whitepaper: No canonical standalone Informal Systems whitepaper or litepaper surfaced in this pass. The clearest current sources of truth were the public audits repository, the Quint audit-services page, and the Model Based Techniques documentation; see ../whitepapers/informal-systems-primary-sources-2026-05-04.md.