Counterflow

Prove the contract, or reveal the exploit.

Counterflow is a smart contract security CLI: AI-translated, machine-proved formal verification for Solidity DeFi contracts — English invariants are checked by a trusted Z3/SMT core, backed by symbolic execution (Halmos, Foundry) and Echidna harness generation for invariant testing. 5 model types, 16 benchmark cases across erc20, amm, lending, staking, oracle, and governance, and 5 real DeFi exploits reproduced ($261M+).

The LLM never decides the verdict. A ~560-line human-auditable Z3 core either proves the invariant for all inputs or produces a concrete counterexample (an exploit trace).

Solidity + English invariants
        │
        ▼
  [LLM translate]          untrusted — DeepSeek/OpenAI, temperature 0
        │
        ▼
  binding.json             human-reviewable artifact (the real spec)
        │
        ▼
  [validate]               deterministic vocabulary/schema gate (5 models, 31 guards, 43 effects, 33 invariants)
        │
        ▼
  [Z3 inductive check]     TRUSTED — 5 model types: erc20_pool, amm_pool, lending_pool, staking_pool, cross_contract
        │
        ▼
  PROVED | VIOLATED (+ cex)   →   audit.jsonl (SHA-256 hash-chained)
        │
        ▼
  [Halmos bytecode]        TRUSTED — EVM symbolic exec (9 scenarios, 3 PASS / 6 FAIL confirming exploits)
  [Foundry fuzz+symb]      fuzz → cex → halmos symbolic proof
  [Echidna validation]     harness generation from binding

State model (5 types)

| Model | Vocab | Guards | Effects | Invariants | |---|---|---|---|---| | erc20_pool | balances, shares, allowances, totals, ghost sums | 11 | 16 | 10 | | amm_pool | reserveX/Y, lpSupply, lpBalances, initialK | 5 | 8 | 5 | | lending_pool | collateral, debt, totals, liqThreshold | 3 | 8 | 8 | | staking_pool | staked, rewards, totalStaked, rewardPool | 2 | 6 | 5 | | cross_contract | cross-in-progress flag, snapshots | 2 | 2 | 1 | | shared extensions | oracle (price, twap), governance (timelock) | 4 | 3 | 4 |

All models share reentrancy vocabulary (lock/snapshot/external-call). The oracle and governance extensions are shared vocabulary usable across models.

Installation

npm install @kryptosai/counterflow
# deps: Python 3 + z3-solver (pip install z3-solver)
# optional: halmos (pip install halmos), Foundry (brew install foundry)
counterflow doctor   # check all deps

Quickstart

counterflow check examples/TokenPool.binding.json      # PROVED
counterflow check examples/TokenPoolBuggy.binding.json # VIOLATED + exploit
counterflow verify Contract.sol invariants.txt         # full AI pipeline (needs API key)
counterflow check binding.json                         # deterministic, no LLM
counterflow bytecode HalmosTest                        # 9 EVM symbolic tests
counterflow bytecode --expect                          # gate: 3 PASS / 6 exploits must reproduce
counterflow audit                                      # verify SHA-256 chain

Use in GitHub Actions

- uses: KryptosAI/counterflow-action@v1
  with:
    binding: path/to/Contract.binding.json

Green on PROVED, red with a counterexample on VIOLATED. Verdict report in the job summary; optional PR comment with github-token: ${{ secrets.GITHUB_TOKEN }}. See counterflow-action.

Leaderboard

Live verification results — benchmark, DeFiHackLabs reproductions, real contract models, ValuePacket — regenerated by CI on every push: kryptosai.github.io/counterflow

Benchmark

16/16 solver cases correct (110-320ms per case):
  erc20_pool: TokenPool†, SafeVault†, TokenPoolBuggy✗, ApprovalDrain✗, UnbackedMintVault✗, BurnDesyncVault✗
  amm_pool:   AMMSwap†, AMMPriceManipulation✗
  lending:    LendingPool†, LendingUnbackedBorrow✗
  staking:    StakingPool†, StakingInfiniteReward✗
  oracle:     OracleSafe†, OracleManipulation✗
  governance: GovernanceTimelock†, GovernanceNoTimelock✗

5/5 DeFiHackLabs real exploits reproduced (deterministic, no LLM):
  FEI Protocol      ($80M)  reentrancy        → reentrancy_safe violated
  CREAM Finance     ($130M) ERC777 reentrancy  → nonneg_balance violated
  PancakeBunny      ($45M)  flash loan         → backing violated
  OpenLeverage      ($230K) access control     → backing violated
  Belt Finance      ($6.3M) arithmetic         → solvency violated

3/3 ValuePacket contracts PROVED at pool level
9/9 Halmos scenarios match expectations (3 PASS / 6 exploits reproduced)
35/35 e2e tests pass

How it works

1. You write invariants in English or Solidity comments
2. LLM translates contract + invariants → structured binding JSON (untrusted layer)
3. Deterministic Z3 core proves or produces a counterexample (trusted layer)
4. Optional Halmos bytecode backstop closes spec-vs-implementation gap
5. SHA-256 hash-chained audit log records every run
6. Optional k-induction: add "init": ["all_zero"] and "induction": {"k": 2} to a binding to also check initiation (BMC from a zero state — a base-case violation is a reachable exploit) and prove the inductive step over k linked transitions (counterflow check handles it automatically; default k=1 is unchanged)

Counterflow vs the landscape

| | Counterflow | Certora Prover | Kontrol | Halmos | |---|---|---|---|---| | Licence | MIT | GPL-3.0 | BSD-3 | AGPL-3.0 | | Input | English | CVL spec | Foundry tests | Foundry tests | | Proof level | Z3 abstract | SMT | KEVM bytecode | Symbolic | | Multi-contract | Yes (cross_contract model + Halmos) | Yes (scene linking) | Yes | Yes | | Model types | 5 (extensible) | Unlimited | Unlimited | N/A | | Bytecode backstop | Halmos + Foundry | No | Native | Native | | Audit chain | SHA-256 | Cloud | No | No | | Setup | npm + Python | Java + Gradle | K + Nix | pip |

What a verdict means

• PROVED — the modeled transition preserves the invariant for all possible inputs
• VIOLATED — Z3 or Halmos found a concrete counterexample (exploit trace)
• UNKNOWN — solver could not decide within limits
• VACUOUS — (per-function flag) the function's guards are unsatisfiable, so its proofs are vacuous; review the binding

Open core (MIT)

CLI, translation prompts, validation, trusted Z3 core, Halmos tests, benchmark bindings, DeFiHackLabs corpus, defi hack runner, ValuePacket verification suite. Commercial layer (separate): hosted pipeline, CI integration, dashboards, proof storage.

Roadmap

• Kontrol integration as second bytecode backstop
• CVL export for Certora Prover interop
• Richer Z3 models: compound interest
• VS Code extension with inline binding review
• Public leaderboard on GitHub Pages