How the AuditHub Approach Would Have Flagged Resupplyfi’s $9.6m Bug: Pre-Mortem

Share this post

Cover image for AuditHub blog post analyzing the $9.6m Resupplyfi bug

Last week’s Auditor’s Take walked through the ResupplyFi bug in detail: an ERC-4626 oracle vulnerable to share-price inflation, a division that rounded down to zero, a solvency check that read the zero as “safe.” $9.6M lost in a single transaction.

This post asks a different question. Could a static analyzer have flagged the pattern before audit? Could a fuzzer have confirmed the exploit before the market opened? With the AuditHub Approach, yes.

What is the AuditHub Approach 

The AuditHub Approach is our systematic detection approach for the classes of vulnerabilities manual review is hard to reason about in an exhaustive way. Generally, this method allows development teams to define automated checks tailored to their protocol in a programmatic way. For DeFi protocol, like ResupplyFi, this is manifested with the following two pillars. 

The first is custom static analysis: per-protocol detectors that flag suspicious structural patterns at commit time. The second is specification-guided fuzzing: running formal invariants against real contract state to confirm whether a flagged pattern is actually exploitable. 

Static analysis is fast and exhaustive but produces false positives. It tells you where a bug could be, not whether it is. Fuzzing is precise but slow without a target. The combination is what makes the method work, and it is what catches bugs of the shape that drained ResupplyFi. 

TL;DR

  • Vanguard, our static analyzer, can flag the suspicious structure: division feeding multiplication through a storage variable in a critical solvency check. 
  • Static-analyzer warnings are not always real bugs. Confirming exploitability needs a dynamic technique like fuzzing. 
  • OrCa, our fuzzer, confirms the bug by exercising the deployed market state against an invariant expressed in our V specification language, producing a counter-example. 
  • Custom static detectors plus specification-guided fuzzing closes the gap between “this code looks suspicious” and “this code is exploitable.” 
  • Both checks are configurable per protocol and re-runnable on every commit. 

How Vanguard can flag the pattern 

Vanguard analyzes Solidity code without running it, matching patterns defined in a user-written detector tailored to the protocol’s logic. For the ResupplyFi class, the shape is roughly: a division whose result eventually feeds a multiplication through a state variable. Here is the custom detector: 

A generic “division before multiplication” detector exists in many Solidity static analyzers. None would have caught this one. They only report the pattern when it appears within a single function on local state. The custom detector above looks across functions and follows the data through a storage variable, both of which are necessary to see the ResupplyFi bug:

Static analysis detects suspicious structural patterns by exhaustively exploring all execution paths in a program. It does not run the code, so it cannot tell you whether the suspicious shape is exploitable, or whether the surrounding logic protects against a potential attack. Some warnings will be false positives. 

That is the cost of working at the structural layer rather than the execution layer. The benefit is that the check runs in seconds on every commit, which is the right cadence for a rate-or-solvency code path that should be considered high-risk by default. Let’s now see how a fuzzer can help us confirm that the above warning is indeed exploitable.

How OrCa confirms the exploit 

OrCa is our fuzzer. It runs against a V Spec, a formal statement of an invariant the contract should preserve. For ResupplyFi, the invariant is straightforward: no borrow should succeed when the resulting loan-to-value ratio exceeds the configured maximum.

The V Spec above is exactly what OrCa ran. It says a user should never complete a borrow or remove-collateral operation where the value of their borrow exceeds the value of their collateral.

For the ResupplyFi market on local deployment, OrCa found a violation to the loan-to-value ratio invariant in under 10 minutes. More on V Spec syntax in the AuditHub documentation. Anyone with the source code and the V Spec can reproduce that locally. Static analysis points at the suspicious path. Fuzzing confirms whether the worry was justified.

A takeaway for developers 

Every lending protocol that prices collateral through an ERC-4626 vault is exposed to the same pattern. Two parts: an oracle path that lets share-price inflation reach the rate calculation, and a solvency check that reads a degenerate rate as safe. 

Both parts are checkable with tooling. Write a custom Vanguard detector for the rate-and-solvency path so any future change to that math is flagged at every commit. Express the LTV invariant as a V Spec and run OrCa against the deployed market before user funds arrive. The alternative is to launch on mainnet after a handful of auditors went over the code in a time-boxed engagement. 

Audit firms can run the same method to scale coverage without scaling the team. If you want to set this up for your protocol, try AuditHub or book a demo to walk through the configuration for your specific market architecture.

Sign up to our newsletter

Stay up to date with the latest news and developments from AuditHub

No spam. Always free. We respect privacy.

About author

Picture of Kostas Ferles

Kostas Ferles

Chief Technology Officer (CTO)

More articles

Security Analysis

How the AuditHub Approach Would Have Flagged Resupplyfi’s $9.6m Bug: Pre-Mortem

AuditHub Announcements

Continuous Formal Verification for ZK Teams Just Got Easier with LLZKV1.0

ZK ecosystem fragmentation forces every language team to rebuild the same security infrastructure from scratch, including compilers, constraint analyzers, and formal verification tooling.
Best Practices

Security Automation: Where Your Web3 Security Time Actually Goes

Discover where your security hours disappear and how security automation can reclaim 15+ weekly hours for architecture decisions.

Ready to automate your security?

Join leading Web3 teams who’ve already embedded continuous security into their development process.

 Get started in 30 minutes / No setup required / See results immediately

See How We Caught Critical Vulnerabilities Others Missed

Get detailed case study showing how formal verification stopped production vulnerabilities

Each case study breaks down actual vulnerabilities we discovered in production code, the mathematical proofs we used to catch them, and the specific verification techniques that prevented exploitation. See the exact tools and methodologies our clients use to ship secure protocols.

“AuditHub has an amazing tool, Picus, which enables RISC Zero to verify and prove the determinism of our ZK circuits. AuditHub integrated into our CI/CD and performs automated checks while we continue making improvements to our code. Amazing work!”

Jeremy Bruestle

CEO & Co-founder at RISC Zero

See How We Caught Critical Vulnerabilities Others Missed

Get detailed case study showing how formal verification stopped production vulnerabilities

Each case study breaks down actual vulnerabilities we discovered in production code, the mathematical proofs we used to catch them, and the specific verification techniques that prevented exploitation. See the exact tools and methodologies our clients use to ship secure protocols.

“AuditHub has an amazing tool, Picus, which enables RISC Zero to verify and prove the determinism of our ZK circuits. AuditHub integrated into our CI/CD and performs automated checks while we continue making improvements to our code. Amazing work!”

Jeremy Bruestle

CEO & Co-founder at RISC Zero