KryptosAI · KryptosAI · Sep 6, 2026 · Sep 6, 2026 · Sep 6, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -33,16 +33,40 @@ jobs:
       - uses: foundry-rs/foundry-toolchain@v1
       - uses: actions/setup-python@v5
         with:
-          python-version: '3.x'
+          python-version: '3.12'
       - run: pip install halmos==0.3.3 z3-solver
       - uses: actions/setup-node@v4
         with:
           node-version: '20.x'
       - run: npm install
+      - name: Require real Forge, Halmos and generated-harness regressions
+        run: node --test test/*.test.js
+        env:
+          COUNTERFLOW_REQUIRE_SYMBOLIC: '1'
       # Expectations gate: safe references must PASS, known exploits must FAIL
       # with a counterexample. Any regression or lost trophy fails the job.
       - run: node src/cli.js bytecode --expect
 
+  certora-local-compile:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+      - uses: actions/setup-node@v4
+        with:
+          node-version: '20.x'
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '21'
+      - run: pip install certora-cli==8.19.1 solc-select
+      - run: solc-select install 0.8.24 && solc-select use 0.8.24
+      # --compilation_steps_only never submits a remote proof or uses a service key.
+      - run: npm run test:cvl
+
   action-smoke:
     runs-on: ubuntu-latest
     steps:

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -2,6 +2,13 @@
 
 All notable changes to Counterflow will be documented in this file.
 
+## Unreleased
+
+- Run original Foundry tests under Halmos instead of generating assertions from counterexamples; preserve exact signatures, setup, failure evidence and full-width witnesses.
+- Fail closed on empty/malformed reports, missing tests, operational failures, timeouts, bounded loops and unsupported invariant sequences. JSON output and CLI exit codes distinguish violations from incomplete checks.
+- Repair concrete Echidna actor tracking and CVL storage-hook exports; report partial coverage and reject vacuous unsigned non-negativity properties.
+- Add real Forge/Halmos and generated-harness regressions, including typed counterexamples, multiple callers and deliberately corrupt accounting.
+
 ## [0.6.1] — 2026-07-23
 
 ### Added

diff --git a/README.md b/README.md
@@ -32,7 +32,7 @@ Solidity + English invariants
         │
         ▼
   [Halmos bytecode]        TRUSTED — EVM symbolic exec (9 scenarios, 3 PASS / 6 FAIL confirming exploits)
-  [Foundry fuzz+symb]      fuzz → cex → halmos symbolic proof
+  [Foundry fuzz+symb]      fuzz → original test under Halmos (bounded checks)
   [Echidna validation]     harness generation from binding
 ```
 
@@ -154,3 +154,43 @@ CLI, translation prompts, validation, trusted Z3 core, Halmos tests, benchmark b
 - Richer Z3 models: compound interest
 - VS Code extension with inline binding review
 - Public leaderboard on GitHub Pages
+
+## Original-test fuzz and symbolic checks
+
+Run `counterflow fuzz-symb AccountingTest --test '^testFuzz_' --root /path/to/foundry-project --json`.
+Forge runs the selected original tests. Each failed ordinary/fuzz test is then run
+under Halmos with its original setup, argument types, operations and assertions.
+No replacement Solidity assertion is fabricated from a counterexample.
+
+Exit codes: **0** for completed fuzzing with no failure (not a symbolic proof),
+**3** whenever Forge observed a violation, **2** for operational or incomplete
+results without a concrete violation. A Halmos pass cannot erase a Forge failure.
+Stateful invariant sequences require a dedicated replay harness and are reported
+unsupported. Empty results, skipped tests, solver timeouts, stuck paths, all-revert
+execution and truncated loops cannot count as symbolic passes. Halmos passes are
+scoped to its configured input/execution bounds.
+
+Both engines use `FOUNDRY_DYNAMIC_TEST_LINKING=false` to preserve native contract
+creation. [Foundry 1.8 enables dynamic test linking by default](https://github.com/foundry-rs/foundry/releases/tag/v1.8.0);
+its injected `deployCode(string)` cheatcode is unsupported by Halmos 0.3.3.
+The runner sets this per process and leaves the project's configuration file intact.
+
+`gen-echidna` and `export-cvl` require `--contract Contract.sol`. Both report
+covered and unsupported invariants and exit 2 on partial coverage. Unsigned
+`>= 0` checks are deliberately unsupported: they cannot witness arithmetic wrap.
+Echidna supports simple contracts without constructor/inheritance setup, scalar
+ABI inputs and concrete solvency/share/backing/cap properties. Use the generated
+wrapper allowlist; delegatecalls preserve caller/storage and track callers plus
+address arguments. Actor-sum checks need manual review if other addresses are
+credited or external callbacks change balances. CVL uses concrete storage hooks
+and getter methods; it omits abstract transition shells without assertions.
+
+Validation: `npm test`, `npm run bench`, `npm run bytecode:expect`.
+Set `COUNTERFLOW_REQUIRE_SYMBOLIC=1` to require installed Forge and Halmos for the
+integration tests instead of allowing their absence to skip those tests.
+
+`npm run test:cvl` compiles and typechecks the generated TokenPool solvency
+specification with Certora CLI 8.19.1, Java 21 and Solidity 0.8.24. Set
+`COUNTERFLOW_SOLC` to the desired compiler executable if it is not `solc` on PATH.
+This check uses `--compilation_steps_only`, needs no service credential and
+submits no remote proof. Remote proof results remain a separate verification step.
diff --git a/bench/halmos-check.js b/bench/halmos-check.js
@@ -24,6 +24,11 @@ console.log('');
 const r = runHalmos('*');
 if (!r.ok) {
   console.error(`${C.red}halmos error: ${r.error}${C.reset}`);
+  for (const result of r.results) {
+    console.error(JSON.stringify({ name: result.name, status: result.status,
+      exitCode: result.exitCode, paths: result.paths, boundedLoops: result.boundedLoops }));
+  }
+  if (r.output) console.error(r.output);
   process.exit(2);
 }
 

diff --git a/package.json b/package.json
@@ -1,14 +1,15 @@
 {
   "name": "@kryptosai/counterflow",
   "version": "0.6.1",
-  "description": "Prove the contract, or reveal the exploit — formal verification for Solidity and DeFi smart contracts. AI-translated invariants proved or refuted by Z3 SMT, with Halmos bytecode backstop and Foundry/Echidna export.",
+  "description": "Prove the contract, or reveal the exploit \u2014 formal verification for Solidity and DeFi smart contracts. AI-translated invariants proved or refuted by Z3 SMT, with Halmos bytecode backstop and Foundry/Echidna export.",
   "main": "src/verify.js",
   "bin": {
     "counterflow": "src/cli.js"
   },
   "scripts": {
     "postinstall": "node -e 'if(process.env.CI||process.env.COUNTERFLOW_SKIP_POSTINSTALL||!process.stdout.isTTY)process.exit(0);console.log(\"Counterflow installed. Run counterflow doctor to check Python 3 + z3-solver setup.\")'",
-    "test": "node test/e2e.js",
+    "test": "node test/e2e.js && node --test test/*.test.js",
+    "test:cvl": "node test/cvl-compile.js",
     "bench": "node bench/run.js",
     "bytecode": "node src/cli.js bytecode HalmosTest",
     "bytecode:expect": "node src/cli.js bytecode --expect",
@@ -27,7 +28,7 @@
     "completeness": "node src/cli.js completeness",
     "mutate": "node src/cli.js mutate",
     "real-contracts": "node src/cli.js check examples/UniswapV2Swap.binding.json && node src/cli.js check examples/AaveLending.binding.json && node src/cli.js check examples/CompoundCToken.binding.json",
-    "cvl-export": "node src/cli.js export-cvl examples/TokenPool.binding.json -o examples/TokenPool.spec"
+    "cvl-export": "node src/cli.js export-cvl examples/TokenPool.binding.json --contract examples/TokenPool.sol -o examples/TokenPool.spec"
   },
   "repository": {
     "type": "git",

diff --git a/src/cli.js b/src/cli.js
@@ -37,10 +37,10 @@ USAGE
   counterflow bench         [--json]
   counterflow audit
   counterflow audit-binding <Contract.sol> [--binding binding.json] [--json]
-  counterflow gen-echidna   <binding.json> [--contract-name Name] [--output-dir path]
+  counterflow gen-echidna   <binding.json> --contract Contract.sol [--contract-name Name] [--output-dir path]
   counterflow gen-foundry   <binding.json> [--contract-name Name] [--output-dir path]
-  counterflow fuzz-symb     <ContractName> [--test TestGlob]
-  counterflow export-cvl    <binding.json> [-o output.spec]
+  counterflow fuzz-symb     <TestContract> [--test TestRegex] [--root path] [--json]
+  counterflow export-cvl    <binding.json> --contract Contract.sol [-o output.spec]
   counterflow kontrol       <TestContract> [--test TestGlob]
   counterflow doctor
   counterflow leaderboard   [--json] [--markdown]
@@ -79,8 +79,13 @@ WHAT A VERDICT MEANS
   UNKNOWN   = solver could not decide within limits.`;
 
 function arg(flag) {
+  // Returns the flag's value, or null when absent OR when the next token is
+  // another flag (missing value) — prevents `--test --json` swallowing --json.
   const i = process.argv.indexOf(flag);
-  return i === -1 ? null : process.argv[i + 1];
+  if (i === -1) return null;
+  const value = process.argv[i + 1];
+  if (value === undefined || value.startsWith('--')) return null;
+  return value;
 }
 
 async function main() {
@@ -244,21 +249,45 @@ async function main() {
     const bindingPath = process.argv[3];
     if (!bindingPath) { console.log(USAGE); process.exit(1); }
     const binding = JSON.parse(fs.readFileSync(bindingPath, 'utf-8'));
-    const contractName = arg('--contract-name') || binding.model || 'Contract';
+    const contractPath = arg('--contract');
+    if (!contractPath) {
+      console.error(`${C.red}gen-echidna requires --contract <Contract.sol> — the old default generated${C.reset}`);
+      console.error(`${C.red}uncompilable harnesses (contract name fell back to the model id).${C.reset}`);
+      process.exit(2);
+    }
+    const resolvedContract = path.resolve(contractPath);
+    if (!fs.existsSync(resolvedContract)) {
+      console.error(`${C.red}contract not found: ${contractPath}${C.reset}`);
+      process.exit(2);
+    }
+    const contractName = arg('--contract-name') || (() => {
+      const { parseContractInfo } = require('./solparse');
+      const names = parseContractInfo(fs.readFileSync(resolvedContract, 'utf-8')).contractNames;
+      return names[0];
+    })();
     const outputDir = path.resolve(arg('--output-dir') || './echidna-output');
     fs.mkdirSync(outputDir, { recursive: true });
 
     const echidna = require('./echidna-gen');
-    const sol = echidna.generateEchidnaTest(binding, contractName);
-    const yaml = echidna.generateEchidnaConfig(binding);
-    const solFile = path.join(outputDir, `Echidna${contractName}.sol`);
+    const importPath = path.relative(outputDir, resolvedContract).replace(/\\/g, '/');
+    let out;
+    try {
+      out = echidna.generateEchidnaTest(binding, resolvedContract, contractName, importPath);
+    } catch (e) {
+      console.error(`${C.red}${e.message}${C.reset}`);
+      process.exit(2);
+    }
+    const yaml = echidna.generateEchidnaConfig(binding, out.filterFunctions || []);
+    const solFile = path.join(outputDir, out.fileName);
     const cfgFile = path.join(outputDir, 'echidna.yaml');
-    fs.writeFileSync(solFile, sol);
+    fs.writeFileSync(solFile, out.sol);
     fs.writeFileSync(cfgFile, yaml);
     console.log(`${C.green}Echidna files generated:${C.reset}`);
     console.log(`  ${solFile}`);
     console.log(`  ${cfgFile}`);
-    process.exit(0);
+    for (const n of out.notes || []) console.log(`  ${C.yellow}${n}${C.reset}`);
+    console.log(`Executable properties: ${out.covered.join(', ')}. Uncovered: ${out.skipped.length}.`);
+    process.exit(out.complete ? 0 : 2);
   }
 
   if (cmd === 'gen-foundry') {
@@ -282,64 +311,50 @@ async function main() {
   }
 
   if (cmd === 'fuzz-symb') {
-    const { spawnSync } = require('child_process');
     const contractName = process.argv[3];
-    if (!contractName) { console.log(USAGE); process.exit(1); }
-    const testGlob = arg('--test') || '*';
-
-    const hasForge = spawnSync('forge', ['--version'], { encoding: 'utf-8' }).status === 0;
-    if (!hasForge) {
-      console.log(`${C.red}forge not installed: install Foundry (https://book.getfoundry.sh)${C.reset}`);
-      process.exit(2);
-    }
-
-    const results = runFuzzThenSymbolic(contractName, testGlob);
-    if (!results.ok) {
-      console.log(`${C.red}${results.error}${C.reset}`);
-      process.exit(2);
-    }
-
-    console.log(`${C.bold}Fuzz + Symbolic Results — ${contractName}${C.reset}`);
-    console.log(`\n${results.combinedSummary}`);
-    console.log(`\n${C.bold}Forge Fuzz:${C.reset}`);
-    console.log(`  exit code: ${results.fuzzResults.exitCode}`);
-    console.log(`  failures: ${results.fuzzResults.failures}`);
-    if (results.fuzzResults.failures > 0) {
-      for (const cex of results.fuzzResults.counterexamples) {
-        console.log(`    ${C.red}${cex.testName}${C.reset}: ${cex.reason}`);
+    if (!contractName || contractName.startsWith('-')) { console.log(USAGE); process.exit(2); }
+    for (const flag of ['--test', '--root']) {
+      if (process.argv.includes(flag) && !arg(flag)) {
+        const error = `${flag} requires a value`;
+        console.log(json ? JSON.stringify({ ok: false, verdict: 'unknown', error }) : error);
+        process.exit(2);
       }
     }
-
-    if (results.symbolicResults.length > 0) {
-      console.log(`\n${C.bold}Halmos Symbolic:${C.reset}`);
-      for (const sr of results.symbolicResults) {
-        const allPassed = sr.halmos.ok && sr.halmos.results.every(r => r.passed);
-        const mark = allPassed ? `${C.green}✓${C.reset}` : `${C.red}✗${C.reset}`;
-        console.log(`  ${mark} ${sr.testName}`);
-        if (!allPassed) {
-          console.log(bytecodeReport(sr.halmos.results));
-        }
+    const result = runFuzzThenSymbolic(contractName, arg('--test'), {
+      cwd: path.resolve(arg('--root') || process.cwd()),
+    });
+    if (json) {
+      console.log(JSON.stringify(result, null, 2));
+    } else if (!result.ok) {
+      console.error(`${C.red}${result.error}${C.reset}`);
+    } else {
+      console.log(result.combinedSummary);
+      for (const sr of result.symbolicResults) {
+        console.log(`  ${sr.status.toUpperCase()} ${sr.cex.contractId}:${sr.cex.signature}`);
+        if (sr.halmos.error) console.log(`    ${sr.halmos.error}`);
+        if (sr.halmos.results.length) console.log(bytecodeReport(sr.halmos.results));
       }
     }
-
-    if (json) console.log(JSON.stringify(results, null, 2));
-    process.exit(results.fuzzResults.failures > 0 ? 3 : 0);
+    process.exit(result.verdict === 'violated' ? 3 : result.ok && result.complete ? 0 : 2);
   }
 
   if (cmd === 'export-cvl') {
     const bindingPath = process.argv[3];
     if (!bindingPath) { console.log(USAGE); process.exit(1); }
     const out = arg('-o') || bindingPath.replace(/\.json$/, '.spec');
+    const contractPath = arg('--contract');
     const cvl = require('./cvl-export');
-    const result = cvl.exportCvl(path.resolve(bindingPath));
+    const result = cvl.exportCvl(path.resolve(bindingPath), contractPath ? path.resolve(contractPath) : null);
     if (!result.ok) {
       console.error(`${C.red}CVL export failed:${C.reset} ${result.error}`);
       process.exit(2);
     }
     fs.writeFileSync(out, result.cvl);
     console.log(`${C.green}CVL spec written to ${out}${C.reset}`);
     console.log(`${C.dim}Model: ${result.model}${C.reset}`);
-    process.exit(0);
+    console.log(`Exported: ${result.covered.join(', ')}. Uncovered: ${result.skipped.length}.`);
+    for (const item of result.skipped) console.log(`  UNSUPPORTED ${item.invariant}: ${item.reason}`);
+    process.exit(result.complete ? 0 : 2);
   }
 
   if (cmd === 'kontrol') {