flexx

Autonomous agents securing crypto companies.

Comment

flexx — Agentic Solidity Smart-Contract Auditor

Inspiration

Smart-contract bugs are irreversible, publicly visible, and devastatingly expensive. Historic exploits like The DAO ($60M drained via reentrancy), Parity Multisig ($150M+ locked via uninitialized library ownership and selfdestruct), and Rubixi (ownership takeover due to a typo in a constructor name) demonstrate that a single line of vulnerable code can destroy an entire protocol.

Yet, existing auditing approaches present a frustrating trade-off:

  1. Static Analyzers & Linters rely on rigid AST pattern-matching. Because they scan code without executing it, they routinely flag already-fixed contracts as vulnerable, generating high false-positive rates that bury real bugs and exhaust developer attention.
  2. LLM-based Auditors generate fluent, convincing vulnerability reports—many of which are complete hallucinations describing non-existent attack vectors. A confident paragraph is not cryptographic or empirical proof.

We asked a fundamental question:
How do we build an AI security auditor whose every claim is provably true—backed by an exploit that actually executes, and a patch that demonstrably stops it?

This inspired flexx: an autonomous agentic auditor where the model plans and reasons, while a deterministic, local EVM execution harness rigorously verifies every single finding through differential execution.

What it does

flexx is a zero-infrastructure, local-first agentic security auditor for Solidity contracts. It replaces single-shot vulnerability guessing with an interactive, verified loop: Plan $\to$ Investigate $\to$ Prove $\to$ Fix $\to$ Re-verify $\to$ Report.

                       ┌───────────────────────────────┐
                       │     Solidity Source Code      │
                       └──────────────┬────────────────┘
                                      │
                                      ▼
                      [ Deterministic Parsing & CFG ]
                     (AST, Call Graph, Path Tracing)
                                      │
                                      ▼
             ┌───────────────── Agent Loop ─────────────────┐
             │                                              │
             │   1. Plan investigation hypotheses           │
             │   2. Inspect functions & trace call paths    │
             │   3. Synthesize Foundry Exploit (PoC)        │
             │   4. Propose code patch                      │
             │                                              │
             └───────────────────────┬──────────────────────┘
                                     │
                                     ▼
                  [ Code-Enforced Differential Gate ]
       Does PoC pass on original?  ──► Yes  ──► (Exploit Confirmed)
       Does PoC fail on patch?     ──► Yes  ──► (Causally Tied Fix)
                                     │
                                     ▼
                    ┌─────────────────────────────────┐
                    │ Verified Differential Report    │
                    │  • report.json / report.md      │
                    │  • Reproducible Foundry PoCs    │
                    │  • Verified remediation patch   │
                    │  • Full reasoning transcript    │
                    └─────────────────────────────────┘

Key Capabilities:

  • Autonomous Multi-Step Investigation: Builds a formal plan, enumerates call paths, tests structural vulnerability candidates, and records discarded false leads.
  • Differential Verification Gate: Rejects vacuous proofs (like require(true)). A finding is accepted if and only if its Foundry Proof-of-Concept (PoC) compiles, passes on the vulnerable contract, and fails on the patched contract.
  • Zero-Hallucination Reporting: Emits comprehensive Markdown and JSON reports where every single vulnerability is accompanied by an executable test case, gas metrics, execution trace, and verified patch.
  • Dual Mode CLI: Runs as a fully autonomous LLM agent (powered by OpenRouter, OpenAI, Groq, or Gemini) or as a deterministic, offline static-analysis engine requiring zero API keys.

How we built it

We designed flexx on a strict architectural principle:

Anything that must be **correct* is deterministic, pure, and unit-tested. Anything that requires judgment is assigned to the model—and checked by the deterministic layer.*

flexx/
├── tools/        # Pure deterministic layer: AST parser, CFG, call graph, Foundry runner, patcher
├── llm/          # Provider-agnostic LLM interface (OpenRouter, OpenAI, Groq, Gemini, Scripted)
├── agent/        # Hand-rolled autonomous loop, tool registry, execution context, state machine
├── report.py     # Differential report generator (JSON & Markdown)
└── eval.py       # Comparative evaluation harness (Single-shot baseline vs. Agent)

1. The Deterministic Analysis Backbone (flexx/tools/)

Before writing any agent logic, we implemented a pure static analysis layer:

  • AST Parsing (parse.py): Uses py-solc-x to construct compilation-unit import graphs and normalized AST representations.
  • Interprocedural CFG & Call Graph (callgraph.py): Employs networkx to build call graphs with labeled internal, external, and delegatecall edges.
  • Path-Sensitive Control-Flow Enumeration (trace.py): Models function execution as structured sequences ($\text{Seq}$), branches ($\text{Branch}$), and loops ($\text{Loop}$), unrolling iterations and inlining modifiers directly at their _; insertion points.
  • Disposable EVM Sandbox (runner.py): Spins up isolated, temporary Foundry projects to compile and execute generated Solidity PoCs, capturing execution traces, revert strings, and exact gas usage.

2. The Agentic Loop & Tool Registry (flexx/agent/)

Rather than relying on opaque agent frameworks (e.g., LangGraph or CrewAI), we engineered a transparent, hand-rolled agent loop with:

  • Strict step caps, per-tool iteration budgets, and retry limits.
  • A clean ToolRegistry exposing inspection tools (trace_path, detect_reentrancy, list_callers) and state-control tools (set_plan, advance_plan_item, submit_finding, finish).
  • Deterministic PoC scaffolds that inject boilerplate (Foundry Vm cheatcodes, pragma declarations, and attack harnesses) so small, fast models do not stumble on syntax details.

3. Mathematical Formulation of Differential Verification

Let $\mathcal{C}$ be the target smart contract, $\mathcal{C}'$ be the patched contract generated by the agent, and $\mathcal{P}$ be the synthesized Foundry Proof-of-Concept exploit test.

The execution outcome of a test $\mathcal{P}$ against contract state $\mathcal{S}$ is modeled as a binary function: $$\text{Run}(\mathcal{P}, \mathcal{S}) = \begin{cases} 1 & \text{if the test executes and passes (exploit succeeds)} \ 0 & \text{if the test reverts or fails compilation} \end{cases}$$

For a security finding to be admitted into the final report with evidence_level: differential, it must satisfy the differential verification condition $\mathcal{V}(\mathcal{P}, \mathcal{C}, \mathcal{C}')$:

$$\mathcal{V}(\mathcal{P}, \mathcal{C}, \mathcal{C}') = \mathbb{I}\Big( \text{Run}(\mathcal{P}, \mathcal{C}) = 1 \;\land\; \text{Run}(\mathcal{P}, \mathcal{C}') = 0 \Big)$$

This guarantees:

  1. True Exploitability: $\text{Run}(\mathcal{P}, \mathcal{C}) = 1$ ensures the contract is genuinely vulnerable under EVM execution semantics.
  2. Causal Efficacy of Patch: $\text{Run}(\mathcal{P}, \mathcal{C}') = 0$ ensures the PoC is not a vacuous identity test (e.g., assert(true)) and that patch $\mathcal{C}'$ specifically eliminates the vulnerability.

4. Non-Vacuous Evaluation Metrics

To honestly evaluate flexx against a single-shot LLM baseline, we formalized benchmark metrics:

$$\text{Precision} = \frac{TP}{TP + FP}, \quad \text{Recall} = \frac{TP}{TP + FN}, \quad \text{FPR} = \frac{FP}{FP + TN}$$

$$\text{Verification Rate } (\mathcal{R}{\text{verif}}) = \frac{|\mathcal{F}{\text{accepted}}|}{|\mathcal{S}_{\text{submissions}}|}$$

$$\text{Differential Rate } (\mathcal{R}{\text{diff}}) = \frac{|\mathcal{F}{\text{diff}}|}{|\mathcal{F}_{\text{reported}}|}$$

where $\mathcal{S}{\text{submissions}}$ represents total finding submission attempts and $\mathcal{F}{\text{accepted}}$ represents findings that survived the EVM execution filter.

Challenges we ran into

1. The Solc AST Serialization Trap

During initial development of our control-flow analyzer, reentrancy detectors produced bizarre false positives and false negatives. We discovered that solc serializes AST JSON node keys alphabetically, rather than in lexical order! For example, ForStatement.body was visited before initializationExpression, and IfStatement.falseBody before trueBody.

  • Solution: We rewrote the AST walker to sort all child nodes strictly by their src source-code byte offsets ($\text{offset}:\text{length}:\text{index}$), ensuring absolute chronological fidelity in state-change and external-call ordering.

2. Path Explosion & Mutually Exclusive Branches

In naive AST scanners, an external call inside an if block and a state update inside the else block are flattened into a single list, triggering false reentrancy alerts.

  • Solution: We implemented structured execution-path enumeration over our CFG, unrolling loops to 0, 1, and 2 iterations to capture loop-carried dependencies while treating mutually exclusive branch arms as isolated execution traces.

3. Guard Heuristics & The Rubixi Incident

When testing against our real-world reproduction of the historic Rubixi exploit (SWC-105), our detector initially failed to identify the vulnerability because an assignment owner = msg.sender inside an unprotected pseudo-constructor was mistaken for an authorization guard.

  • Solution: We refined our modifier and guard recognition heuristics to distinguish between variable reads used as predicate constraints (require(msg.sender == owner)) and unconstrained state writes, immediately surfacing the ownership takeover vector.

Accomplishments that we're proud of

  • 100% Differential Precision on Real-World Benchmark: Evaluated on faithful reproductions of historic exploits (The DAO [SWC-107], Phishable [SWC-115], Rubixi [SWC-105], and Parity Suicidal Wallet [SWC-106]), flexx achieved:
    • $\text{Precision} = 1.0$
    • $\text{False Positive Rate (FPR)} = 0.0$ on all fixed/clean contract counterparts
    • $\mathcal{R}_{\text{diff}} = 1.0$ (every reported finding was differentially proven).
  • Beating the Baseline: While the single-shot LLM baseline continued to hallucinate vulnerabilities on clean/fixed contracts, flexx's EVM verification gate completely eliminated false alarms.
  • 100+ Offline Automated Tests: Engineered an entirely offline testing suite using a deterministic scripted mock LLM backend that validates AST analysis, call-graph construction, tool dispatch, and report generation without requiring network access or incurring API costs.
  • Zero-Infra CLI Tooling: Packaged as an instant-run CLI via pipx, uvx, and npx, giving smart contract developers a seamless tool for CI/CD and local development.

What we learned

  1. Verification is the Heart of Agentic Coding: An LLM without a verification environment is merely an essayist. Giving the model a deterministic execution runtime (Foundry) transforms it from an unreliable pattern-matcher into a rigorous reasoning engine.
  2. The Patch is the Control Condition: A remediation patch is not just an advisory recommendation—it serves as the mathematical negative control required to confirm that an exploit PoC is genuine.
  3. Honest System Boundaries Matter: Instead of pretending our static detectors can magically discover every arbitrary zero-day, flexx explicitly demarcates structurally covered patterns from open-ended model hypotheses, maintaining integrity across all reports.

What's next for flexx

  • Expanded Exploit Scaffolds: Introducing deterministic detector models and PoC synthesizers for flash-loan price manipulation, read-only reentrancy across ERC-4626 vaults, and arbitrary delegatecall storage collisions.
  • Agent-Guided Invariant Fuzzing: Connecting the agent loop to Foundry's invariant testing engine and Echidna, allowing flexx to synthesize custom property invariants and guide coverage-based fuzzing.
  • Multi-Contract Protocol Audits: Scaling the CFG and call-graph analyzer to support cross-contract inheritance hierarchies, proxy patterns (UUPS/Transparent), and multi-repository DeFi ecosystems.
  • Automated CI/CD Security Gate: Releasing an official GitHub Action that runs differential audit passes on pull requests, blocking merges only when a reproducible exploit is proven.

Built With

Share this project:

Updates