RedMirror_

An exhaustive state-space verification oracle to harden your security stack.

function withdraw(uint amt) {
  require(balance[user] >= amt);
  user.call{value: amt}("");

  balance[user] -= amt;
}

function withdraw(uint amt) {
  require(balance[user] >= amt);
  user.call{value: amt}("");   // sent before the balance is updated  // if this crashes, the balance is never updated
  balance[user] -= amt;
}

We offer model-driven security audits. RedMirror models your critical subsystems as state machines and exhaustively explores every reachable state, returning either a concrete, reproducible vulnerability (the exact path that triggers it) or, when none surfaces, a precise account of what was checked and how far. Across nine languages and smart contracts.

In the wild

Fixes and findings RedMirror surfaced in major OSS projects:

• PrefectHQ/prefect #21829 (PR, merged): cycle detection for block_document references
• PrefectHQ/prefect #21794 (issue): concurrency-slot leak from swallowed exceptions in V2 lease release / cleanup paths
• eznix86/mailgun-proxy-for-ghost #17 (merged): deny access when the Mailgun API key is unset
• apache/airflow #67076 (merged): leftover temp report file in BidManager download
• apache/airflow #67075: IMAP hook hardened against symlink-followed writes
• apache/airflow #67074: Kubernetes executor config isolated from the global default

Beyond the public fixes above, many findings have been disclosed privately through HackerOne, Bugcrowd, and Cantina.xyz, on programs including Polymarket, Mattermost, and Reserve Governor, among many others.