Informal Systems

• Name: Informal Systems
• URL: https://informal.systems/
• Category: protocol-assurance and formal-verification company / audit-methodology and tooling operator / distributed-systems security workflow steward
• Summary: Informal Systems belongs in companies/, not only projects/, because the practical leverage is not just one modeling tool or one audit report. The useful question is who packages model-based verification, behavioral auditing, CI-pluggable assurance harnesses, and a public report corpus into a repeatable security workflow that downstream protocols start treating as a serious review standard. That authority sits with Informal Systems as a named organization more clearly than with any one repo.
• What it does:
  • Operates a protocol-security and verification practice centered on system behavior, formal methods, and distributed-systems assurance rather than only manual code review
  • Publishes a substantial public audit-report corpus across IBC-adjacent systems, dYdX, Celestia, Neutron, Namada, Osmosis, Ripple, Zenrock, and other distributed-system clients
  • Develops and maintains first-party modeling and verification tools such as Quint, Apalache, Modelator, and cosmwasm-to-quint
  • Frames audit delivery around model construction, property verification, model-based testing, and comparison against implementation and production traces
  • Packages reusable verification harnesses and methods that can persist after a point-in-time engagement, which makes the company boundary analytically stronger than a single audit artifact
• Key claims:
  • Informal says it was founded to build trust in software and monetary systems and specializes in secure, interoperable, and fault-tolerant networks
  • The public audits repository says Informal applies a multi-layered, automated approach to blockchain security audits under researchers in protocol design, verification, and testing
  • The same audits repository explicitly names first-party tools such as Quint, Apalache, and Atomkraft as part of the assurance stack and shows a long multi-client public report history
  • Informal’s audit-services material says it audits system behavior, not just code, by modeling intended behavior, verifying properties across possible states, and comparing those properties against implementation and production execution
  • The same audit-services material says customers receive a verification harness that plugs into CI so critical security properties can keep being checked after the initial engagement
  • The Model Based Techniques docs say Informal uses model-based techniques both in its own development practice and in security audit services, and list Quint, Apalache, Modelator, and cosmwasm-to-quint as first-party tools
• Whitepaper: No classic standalone company whitepaper is the point here. The useful primary materials are the audits repository, the audit-services materials, the Model Based Techniques docs, and the existing source bundle in ../whitepapers/informal-systems-primary-sources-2026-05-04.md.
• Sources:
  • https://informal.systems/
  • https://raw.githubusercontent.com/informalsystems/audits/main/README.md
  • https://quint.sh/audits
  • https://mbt.informal.systems/

Internal linkages

• Project-layer note: informal-systems.
• Strong adjacent company reads: trail-of-bits, openzeppelin, and chainsecurity.
• Useful product-level comparison where tooling becomes the main unit rather than the company shell: certora.

Protocol / company boundary

• informal-systems is the project-layer note for the reusable assurance surface: public reports, modeling tools, and the protocol-facing verification stack teams can build around directly.
• This company note is the operator boundary: Informal chooses how those methods are packaged, which assurance language becomes canonical in its engagements, how the public report corpus is curated, and how much downstream teams inherit CI-oriented verification workflow from Informal-authored systems.
• That split matters because the dependency sophisticated clients inherit is often not just formal methods exist; it is Informal's method bundle, report style, tooling stack, and review posture became part of the live engineering workflow.

Control surface

• Practical leverage sits in methodology branding, audit-scope framing, property-selection discipline, verification-harness packaging, public-report publication norms, and which first-party tools or modeling practices clients are pushed to normalize in production engineering.

• Even when the tools are open source, the company still shapes the onboarding path, the authoritative language around behavioral assurance, and the way protocol teams operationalize formal verification after audits end.

• Read the durable choke point here as who turns formal methods into a repeatable workflow that protocols actually adopt?, not only which model checker exists?

• Last reviewed: 2026-08-06 UTC