Informal Systems primary sources — 2026-05-04

Project status in this pass

• No canonical standalone Informal Systems whitepaper or litepaper surfaced.
• The clearest current source of truth is the public audits repository plus Informal’s Quint audit-services page and Model Based Techniques documentation.
• The project is best understood as formal-verification and protocol-assurance infrastructure rather than as a simple audit boutique.

Primary-source snapshots

1) Public audits repository

• URL: https://raw.githubusercontent.com/informalsystems/audits/main/README.md
• Key excerpt:
  • The README says Informal Systems applies a multi-layered, automated approach to blockchain security audits under researchers in protocol design, verification, and testing.
  • It explicitly names first-party tools such as Quint, Apalache, and Atomkraft as part of the assurance stack.
  • The repo maintains a long public list of audit reports spanning IBC, dYdX, Celestia, Neutron, Osmosis, Namada, Ripple, Zenrock, and other projects.

2) Quint audit-services page

• URL: https://informal.systems/security
• Final URL observed during retrieval: https://quint.sh/audits
• Key excerpt:
  • The page says Informal audits system behavior, not just code.
  • It says the team models intended behavior, verifies properties across possible states, and compares the result against both implementation and production execution.
  • It also says customers receive a verification harness that plugs into CI for continuous checking of critical security properties.

3) Model Based Techniques documentation

• URL: https://mbt.informal.systems/
• Key excerpt:
  • The docs say Informal uses model-based techniques both in its development practice and in security audit services.
  • It lists first-party tools including Quint, Apalache, Modelator, and cosmwasm-to-quint.
  • The page says Informal was founded to build trust in software and monetary systems and specializes in secure, interoperable, and fault-tolerant networks.

4) Official homepage

• URL: https://informal.systems/
• Key excerpt:
  • The homepage was minimally extractable in this pass, but it remains the canonical company URL and aligns with the broader mission language repeated on other first-party properties.

Working conclusion

Informal Systems is best cataloged as formal-verification and protocol-assurance infrastructure. The deciding evidence in this pass was the combination of a public multi-year audit corpus, explicit model-based verification language, first-party verification tools, and a CI-oriented assurance posture that goes beyond conventional point-in-time audit delivery.