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@v1with:
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