My name is RJ Lopez. Six weeks ago I knew nothing about smart contracts, security research, or software development.

I've spent those six weeks building VERITAS Ω — an 8-gate verification engine for smart contract security analysis — and deploying it as EasyStreet, a self-service audit platform at aegisaudits.com. Last week I ran the real pipeline against Euler Finance's EToken.sol, the contract at the center of a $197M exploit in March 2023.

I'm publishing the exact machine output. Not a marketing teardown. Not a curated demo. The real result, the real gaps, and the honest explanation of why those gaps exist.

This is what intellectual honesty looks like in security tooling. I think the space needs more of it.

EasyStreet runs submitted source code through 8 sequential verification gates:

INTAKE → TYPE → EVIDENCE → AUTHORITY → SOLVENCY → INCENTIVE → TEMPORAL → ADVERSARY

Each gate produces a binary verdict: PASS or VIOLATION. No scoring. No "medium severity" hedging. If a gate fires, the terminal verdict is VIOLATION and the audit terminates with an evidence package — a PDF report, a machine-readable JSON artifact, and a SHA-256 root commitment.

The framework is built on two layers:

• Slither (Trail of Bits' open-source static analyzer) for pattern-level findings

• VERITAS custom detectors for gate-specific invariant checks

Every report is deterministic and replayable. Same input, same SHA-256, same output, forever.

Protocol: Euler Finance v1
Contract: EToken.sol → donateToReserves()
Attack: Flash loan → donation attack → self-liquidation
Loss: $197M (DAI, WETH, WBTC, stETH, USDC)
Date: March 13, 2023 (Block 16818057)
Root cause: Missing checkLiquidity() call in donateToReserves()

The attack in five steps:

1. Flash loan $30M DAI from Aave

2. Deposit $20M → get eDAI tokens

3. mint() leveraged position → eDAI + dDAI at 10x

4. donateToReserves(100M eDAI) — burns eTokens, NOT dTokens

5. Self-liquidate insolvent position → extract $197M, repay flash loan

The critical flaw: donateToReserves() calls burnTokens() on the sender's eDAI balance but never calls checkLiquidity(). The attacker can intentionally make their position insolvent without triggering any health factor checks, then liquidate at a manipulated exchange rate.

Target:    EToken.sol (Euler Finance v1)
SHA-256:   e16bcbe5efa32f3b0538ed3f6ec29a2d64dbbff622b9712d129191731a79cd8b
Slither:   v0.11.5
VERITAS:   v1.0.0
Gate eval: 0.04ms
Timestamp: 2026-03-13T20:51:27.181397+00:00

======================================================================
  VERITAS Omega -- EASYSTREET GATE REPORT
======================================================================
  Target:   EToken.sol
  SHA-256:  e16bcbe5efa32f3b0538ed3f6ec29a2d...
            64dbbff622b9712d129191731a79cd8b
  Time:     2026-03-13T20:51:27.181397+00:00
  Slither:  0.11.5
  VERITAS:  1.0.0
----------------------------------------------------------------------
  [INTAKE]    PASS
  [TYPE]      ** VIOLATION **
    Reason: NONDETERMINISTIC_COMPILER
      - [VERITAS] floating_pragma @ L3
        pragma solidity ^0.8.0;
        CWE-710 / SWC-103

  [EVIDENCE]  ** VIOLATION **
    Reason: EVIDENCE_CHAIN_INCOMPLETE
      - [VERITAS] missing_event @ L126 — touch()
      - [VERITAS] missing_event @ L279 — approveSubAccount()
        CWE-778

  [AUTHORITY] ** VIOLATION **
    Reason: AUTHORITY_BOUNDARY_COMPROMISED
      - [VERITAS] missing_access_control @ L180 — withdraw()
      - [VERITAS] missing_access_control @ L206 — mint()
      - [VERITAS] missing_access_control @ L234 — burn()
      - [VERITAS] missing_access_control @ L306 — transfer()
        CWE-284 / SWC-105

  [SOLVENCY]  ** VIOLATION **
    Reason: SOLVENCY_STATE_MUTABLE
      - [VERITAS] unchecked_math @ L162 — deposit unchecked block
      - [VERITAS] unchecked_math @ L339 — allowance subtraction
      - [VERITAS] unchecked_math @ L376 — donateToReserves balance
        CWE-190 / SWC-101

  [INCENTIVE] PASS
  [TEMPORAL]  PASS
  [ADVERSARY] PASS
----------------------------------------------------------------------
  GATES PASSED:   INTAKE, INCENTIVE, TEMPORAL, ADVERSARY
  GATES VIOLATED: TYPE, EVIDENCE, AUTHORITY, SOLVENCY
  TOTAL FINDINGS: 10
  TERMINAL VERDICT: ** VIOLATION **
  ROOT COMMITMENT:  sha256:34959ecb44f068c0a85976f4a3ff8bda
                          6e30802fe491913c93d81cd02887d5aa
======================================================================

The bottom line: a customer submitting Euler's EToken.sol to EasyStreet would receive a VIOLATION verdict before deployment.

Here is exactly where the real output diverged from a complete analysis of the exploit — and why.

The terminal verdict is correct. The specific mechanisms the pipeline caught differ from the actual exploit path in three gates and miss it entirely in two.

Slither returned 0 findings.
EToken.sol imports ../BaseLogic.sol which wasn't on disk. Slither requires the full dependency tree to compile and analyze. On a real AEGIS audit, the customer uploads the full project or we pull the full repo. Single-file analysis disables Slither entirely.

INCENTIVE gate didn't fire.
The flash_loan_surface detector searches for patterns like IFlashLoan, flashLoan(, executeOperation(, onFlashLoan(. None of these appear in EToken.sol. The flash loan lives in the attacker's contract, not the victim's. Catching this pattern requires cross-contract taint analysis — tracing that donateToReserves() can be called mid-flash-loan from an external contract. The current regex scanner can't do that.

ADVERSARY gate didn't fire.
The governance_risk detector looks for propose(), execute(), votingDelay, quorum. The proxy_safety detector looks for delegatecall, upgradeTo, ERC1967, initializ. None of these appear in EToken.sol because the proxy and governance infrastructure lives in Euler's deployment framework, not the module itself. Catching this requires dependency-aware analysis of the full deployment context.

donateToReserves() wasn't flagged for missing access control.
The missing_access_control detector checks against a hardcoded keyword list: withdraw, mint, burn, transfer, setOwner, upgrade. The function name donateToReserves isn't in that list. This is a detector coverage gap. The function is sensitive — it modifies collateral without a solvency check — but the detector doesn't recognize it by name. Semantic function classification would catch it; name matching doesn't.

The 8-gate framework correctly partitioned the analysis space. The terminal verdict was correct. The gaps are detector depth problems, not architectural failures.

Here's the engineering roadmap those gaps write directly:

1. Full-project analysis
Require full repo upload or pull from GitHub/Etherscan. This unlocks Slither's complete detection surface and is the single highest-leverage improvement available.

2. Semantic function classification
Replace name-matching for access control detection with a semantic classifier that identifies functions as sensitive based on what state they modify, not what they're named. donateToReserves() modifies collateral balances — that's the signal, not the name.

3. Cross-contract taint analysis
Track whether a public state-mutating function can be called within a flash loan callback from an external contract. This is the pattern class that catches Euler, Wormhole-style attacks, and most DeFi flash loan exploits.

4. Deployment-context governance detection
Analyze the proxy and upgrade infrastructure alongside the target contract, not just the target in isolation.

These are scoped engineering improvements with clear justification. They're on the roadmap.

Security tooling marketing consistently oversells what automated analysis can do. Most vendors show you the catches and hide the misses.

I think that's wrong. The security community deserves to know exactly what a tool covers and where it stops. Researchers building on top of tools like this need the honest coverage map, not the marketing version.

EasyStreet caught 4/8 gates on a single-file analysis with no dependency resolution and still produced the correct terminal verdict. With full-project input, Slither enabled, and the three detector improvements above, the coverage on this class of exploit becomes substantially more complete.

If you want to run your own contract through the pipeline, the free tier is live at aegisaudits.com. The full 8-gate audit with evidence package and SHA-256 seal is $299.

If you're a security researcher and want to talk about the framework, the detector gaps, or anything in this post — I'm at RJ@AegisAudits.com.

EasyStreet by VERITAS Ω — Formal Verification · SHA-256 · aegisaudits.com
RJ Lopez | Veritas Vault Security Research