@kryptosai/counterflow - npm Package Compare versions

Comparing version 0.4.2 to 0.5.0

bench/halmos-check.js

+#!/usr/bin/env node
+/**
+ * Halmos expectations check — runs the HalmosTest suite and compares results
+ * against halmos/expectations.json. Exit 0 iff every expectation matches.
+ * Safe references must PASS; known exploits must FAIL with a counterexample.
+ */
+const fs = require('fs');
+const path = require('path');
+const { runHalmos } = require('../src/halmos-runner');
+const { compareExpectations } = require('../src/halmos-expect');
+
+const C = {
+  reset: '\x1b[0m', bold: '\x1b[1m', dim: '\x1b[2m',
+  red: '\x1b[31m', green: '\x1b[32m', yellow: '\x1b[33m',
+};
+
+const expPath = path.join(__dirname, '..', 'halmos', 'expectations.json');
+const exp = JSON.parse(fs.readFileSync(expPath, 'utf-8'));
+
+console.log('');
+console.log(`${C.bold}Counterflow Halmos expectations check${C.reset} ${C.dim}(${exp.scenarios.length} scenarios, halmos ${exp.halmos_version})${C.reset}`);
+console.log('');
+
+const r = runHalmos('*');
+if (!r.ok) {
+  console.error(`${C.red}halmos error: ${r.error}${C.reset}`);
+  process.exit(2);
+}
+
+const { ok, matches, mismatches } = compareExpectations(exp.scenarios, r.results);
+
+for (const m of matches) {
+  console.log(`  ${C.green}✓${C.reset} ${m.name}  ${C.dim}[${m.class}] ${m.outcome}${C.reset}`);
+}
+for (const m of mismatches) {
+  console.log(`  ${C.red}✗${C.reset} ${m.name}`);
+  console.log(`      ${C.red}${m.problem}${C.reset}`);
+  if (m.counterexample) {
+    console.log(`      ${C.dim}cex: ${JSON.stringify(m.counterexample)}${C.reset}`);
+  }
+}
+console.log('');
+console.log(`  ${matches.length}/${matches.length + mismatches.length} expectations matched`);
+console.log('');
+process.exit(ok ? 0 : 1);

halmos/expectations.json

+{
+  "description": "Expected Halmos outcomes for halmos/test/HalmosTest.t.sol. PASS = safe reference must keep passing. FAIL = exploit must stay reproducible (with a counterexample). Any mismatch fails the check: a FAIL-turned-PASS is a lost trophy (halmos or the contract changed), a PASS-turned-FAIL is a regression.",
+  "halmos_version": "0.3.3",
+  "scenarios": [
+    { "name": "check_TokenPool_withdraw_noUnderflow", "expect": "pass", "class": "reference", "why": "safe pool: withdraw can never drive balance below its previous value" },
+    { "name": "check_TokenPoolBuggy_withdraw_noUnderflow", "expect": "fail", "class": "underflow-drain", "why": "missing balance check: withdraw underflows the balance" },
+    { "name": "check_SafeVault_withdraw_shareIntegrity", "expect": "pass", "class": "reference", "why": "safe vault: totalShares tracks totalAssets across withdraw" },
+    { "name": "check_SafeVault_accounting_multiOp", "expect": "pass", "class": "reference", "why": "safe vault: multi-op accounting keeps totals non-negative" },
+    { "name": "check_UnbackedMintVault_ownerMint", "expect": "fail", "class": "unbacked-mint", "why": "owner mint inflates shares without assets: backing violated" },
+    { "name": "check_BurnDesyncVault_burn", "expect": "fail", "class": "accounting-desync", "why": "burn forgets totalShares: shares outgrow assets" },
+    { "name": "check_ApprovalDrain_allowance_respected", "expect": "fail", "class": "approval-drain", "why": "unchecked allowance math: approve(1) allows draining the full balance" },
+    { "name": "check_ReentrantVault_backing_violated", "expect": "fail", "class": "reentrancy", "why": "transfer-before-state-update lets the attacker drain without burning shares" },
+    { "name": "check_FlashLoanPool_repayment_required", "expect": "fail", "class": "flash-loan", "why": "flash loan never checks repayment: pool drained during callback" }
+  ]
+}

src/halmos-expect.js

+/**
+ * Compare actual Halmos results against halmos/expectations.json.
+ *
+ * Pure function — no halmos dependency, fully unit-testable.
+ *
+ * Outcomes per scenario:
+ *   expect pass + passed                → match
+ *   expect fail + failed (with cex)     → match (exploit stays reproducible)
+ *   expect fail + failed (no cex)       → mismatch (unverifiable failure)
+ *   expect pass + failed                → mismatch (REGRESSION)
+ *   expect fail + passed                → mismatch (LOST TROPHY)
+ *   name only in expectations           → mismatch (missing scenario)
+ *   name only in results                → mismatch (unregistered scenario)
+ */
+
+function stripSig(name) {
+  // halmos prints e.g. "check_Foo_bar(uint256,uint256)" — expectations use bare names
+  return String(name).replace(/\(.*$/, '');
+}
+
+function compareExpectations(expectedScenarios, actualResults) {
+  const matches = [];
+  const mismatches = [];
+  const actualByName = new Map(actualResults.map((r) => [stripSig(r.name), r]));
+  const expectedNames = new Set();
+
+  for (const e of expectedScenarios) {
+    const key = stripSig(e.name);
+    expectedNames.add(key);
+    const a = actualByName.get(key);
+    if (!a) {
+      mismatches.push({ name: key, problem: 'expected scenario not found in halmos results' });
+      continue;
+    }
+    if (e.expect === 'pass') {
+      if (a.passed) {
+        matches.push({ name: key, outcome: 'pass', class: e.class });
+      } else {
+        mismatches.push({ name: key, problem: 'REGRESSION: expected PASS but halmos FAILED', counterexample: a.counterexample });
+      }
+    } else if (!a.passed) {
+      const hasCex = a.counterexample && Object.keys(a.counterexample).length > 0;
+      if (hasCex) {
+        matches.push({ name: key, outcome: 'fail (exploit reproduced)', class: e.class });
+      } else {
+        mismatches.push({ name: key, problem: 'expected FAIL with counterexample but failed without one' });
+      }
+    } else {
+      mismatches.push({ name: key, problem: 'LOST TROPHY: expected FAIL (exploit) but halmos PASSED — investigate halmos/contract changes' });
+    }
+  }
+
+  for (const r of actualResults) {
+    const key = stripSig(r.name);
+    if (!expectedNames.has(key)) {
+      mismatches.push({ name: key, problem: 'unregistered halmos scenario — add it to halmos/expectations.json' });
+    }
+  }
+
+  return { ok: mismatches.length === 0, matches, mismatches };
+}
+
+module.exports = { compareExpectations, stripSig };

CHANGELOG.md

@@ -5,2 +5,16 @@ # Changelog
 
+## [0.5.0] — 2026-07-22
+
+### Added
+
+- **K-induction (opt-in)**: bindings may add `"init": ["all_zero"]` and `"induction": {"k": 2}` (k ≤ 5). The solver then checks initiation by bounded model checking from a zero deploy state (a base-case violation is a *reachable* exploit, reported with its depth) and proves the step over k linked transitions of the full multi-function transition relation. Default k=1 is byte-identical to previous behavior. Output carries `proof` metadata for both modes.
+- **Halmos expectations harness**: `halmos/expectations.json` is the versioned registry of the 9 bytecode scenarios (3 safe references must PASS, 6 exploits must FAIL with a counterexample). `counterflow bytecode --expect` / `bench/halmos-check.js` gates on it: regressions, lost trophies, and unregistered scenarios all fail the check. Runs in CI as a required job.
+- `serve --port 0` support (OS-assigned ephemeral port; CLI prints the actual bound port) plus a clean EADDRINUSE error.
+- e2e: 9 new tests (halmos comparator ×4, k-induction ×5) and the serve test now uses an ephemeral port — 35/35 pass.
+
+### Fixed
+
+- `runHalmos('*')` passed a literal `*` to halmos's regex contract filter, silently producing zero results; `*`/empty now omits the filter (runs all test contracts).
+- Halmos counterexample parsing: halmos prints the cex block *before* the `[FAIL]` line; vars were mis-attributed to the previous result. Parser now buffers and attaches correctly.
+
 ## [0.4.2] — 2026-07-22
@@ -7,0 +21,0 @@

package.json

 {
   "name": "@kryptosai/counterflow",
-  "version": "0.4.2",
+  "version": "0.5.0",
   "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.",
@@ -14,2 +14,3 @@ "main": "src/verify.js",
     "bytecode": "node src/cli.js bytecode HalmosTest",
+    "bytecode:expect": "node src/cli.js bytecode --expect",
     "defihack:clone": "bash bench/defihack/setup.sh",
@@ -84,2 +85,3 @@ "defihack:bench": "node bench/defihack/runner.js",
     "halmos/foundry.toml",
+    "halmos/expectations.json",
     "slither/*.py",
@@ -86,0 +88,0 @@ "valuepacket",

README.md

@@ -68,2 +68,3 @@ # <picture><img src="assets/logo.png" height="48" align="left" alt="Counterflow logo"/></picture>Counterflow
 counterflow bytecode HalmosTest                        # 9 EVM symbolic tests
+counterflow bytecode --expect                          # gate: 3 PASS / 6 exploits must reproduce
 counterflow audit                                      # verify SHA-256 chain
@@ -91,3 +92,4 @@ ```
 3/3 ValuePacket contracts PROVED at pool level
-26/26 e2e tests pass
+9/9 Halmos scenarios match expectations (3 PASS / 6 exploits reproduced)
+35/35 e2e tests pass
 ```
@@ -102,2 +104,6 @@
 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)
 
@@ -104,0 +110,0 @@ ## Counterflow vs the landscape

solver/check.py

@@ -10,7 +10,22 @@ #!/usr/bin/env python3
 staking_pool, cross_contract.
+
+Proof modes (binding.induction.k):
+    k=1 (default) — 1-induction per function (preservation only).
+    k=2..5        — k-induction over the whole transition relation, with
+                    initiation checked by BMC from binding.init (e.g.
+                    "init": ["all_zero"]). Opt-in; requires a non-empty
+                    init block.
 """
 import json, sys
-from models import check_function, check_vacuity, GUARDS, EFFECTS, INVARIANTS
+from models import (
+    check_function, check_vacuity, check_k_induction,
+    GUARDS, EFFECTS, INVARIANTS, INIT_PREDS,
+)
 
 
+def fail(msg):
+    print(json.dumps({"error": msg}))
+    sys.exit(2)
+
+
 def main():
@@ -21,8 +36,51 @@ raw = sys.stdin.read()
     invariants = binding.get("invariants", [])
+    init_names = binding.get("init", []) or []
+    induction = binding.get("induction", {}) or {}
+    k = induction.get("k", 1)
 
     for inv in invariants:
         if inv not in INVARIANTS:
-            print(json.dumps({"error": f"unknown invariant: {inv}"}))
-            sys.exit(2)
+            fail(f"unknown invariant: {inv}")
+    for name in init_names:
+        if name not in INIT_PREDS:
+            fail(f"unknown init predicate: {name}")
+    if not isinstance(k, int) or isinstance(k, bool) or k < 1 or k > 5:
+        fail("induction.k must be an integer between 1 and 5")
+    if k > 1 and not init_names:
+        fail('induction.k > 1 requires a non-empty init block (e.g. "init": ["all_zero"])')
+    if init_names and k == 1:
+        print("warning: init block present but induction.k=1 — init unused; "
+              "set induction.k >= 2 to enable k-induction", file=sys.stderr)
 
+    funcs = binding.get("functions", [])
+    for func in funcs:
+        for g in func.get("guards", []):
+            if g not in GUARDS:
+                fail(f"unknown guard: {g}")
+        for e in func.get("effects", []):
+            if e not in EFFECTS:
+                fail(f"unknown effect: {e}")
+
+    vacuity = []
+    for func in funcs:
+        v = check_vacuity(func, invariants, model=model)
+        if v:
+            print(f"warning: function '{func['name']}' has unsatisfiable guards — proofs are vacuous",
+                  file=sys.stderr)
+        vacuity.append({"function": func["name"], "vacuous": v})
+
+    if k > 1:
+        ki = check_k_induction(funcs, invariants, model, init_names, k)
+        any_violation = any(r["status"] == "violated" for r in ki["invariants"])
+        any_unknown = any(r["status"] == "unknown" for r in ki["invariants"])
+        verdict = "violated" if any_violation else ("unknown" if any_unknown else "proved")
+        print(json.dumps({
+            "verdict": verdict,
+            "model": model,
+            "proof": {"kind": "k-induction", "k": k, "init": init_names},
+            "invariants": ki["invariants"],
+            "functions": vacuity,
+        }, indent=2))
+        return
+
     func_results = []
@@ -32,11 +90,3 @@ any_violation = False
 
-    for func in binding.get("functions", []):
-        for g in func.get("guards", []):
-            if g not in GUARDS:
-                print(json.dumps({"error": f"unknown guard: {g}"}))
-                sys.exit(2)
-        for e in func.get("effects", []):
-            if e not in EFFECTS:
-                print(json.dumps({"error": f"unknown effect: {e}"}))
-                sys.exit(2)
+    for i, func in enumerate(funcs):
         results = check_function(func, invariants, model=model)
@@ -48,6 +98,5 @@ for r in results:
                 any_unknown = True
-        vacuous = check_vacuity(func, invariants, model=model)
-        if vacuous:
-            print(f"warning: function '{func['name']}' has unsatisfiable guards — proofs are vacuous", file=sys.stderr)
-        func_results.append({"function": func["name"], "vacuous": vacuous, "results": results})
+        func_results.append({"function": func["name"],
+                             "vacuous": vacuity[i]["vacuous"],
+                             "results": results})
 
@@ -61,3 +110,8 @@ if any_violation:
 
-    print(json.dumps({"verdict": verdict, "model": model, "functions": func_results}, indent=2))
+    print(json.dumps({
+        "verdict": verdict,
+        "model": model,
+        "proof": {"kind": "1-induction", "k": 1},
+        "functions": func_results,
+    }, indent=2))
 
@@ -64,0 +118,0 @@

solver/models.py

@@ -42,3 +42,3 @@ """
 from z3 import (
-    Int, Array, IntSort, Select, Store, ForAll, Implies, And, Not,
+    Int, Array, IntSort, Select, Store, ForAll, Implies, And, Or, Not,
     Solver, sat, unsat, IntVal, K,
@@ -504,38 +504,41 @@ )
 
-def _build_pre_state(model):
+def _build_pre_state(model, sfx="pre"):
+    # sfx="pre" reproduces the historical variable names exactly; k-induction
+    # chains use sfx="s0".."s{k}" for per-link states.
     return State(
-        Int("totalAssets_pre"), Int("totalShares_pre"),
-        Array("balances_pre", IntSort(), IntSort()),
-        Array("shares_pre", IntSort(), IntSort()),
-        Array("allowances_pre", IntSort(), IntSort()),
-        Int("sumBalances_pre"), Int("sumShares_pre"),
-        locks=Array("locks_pre", IntSort(), IntSort()),
-        in_call=Int("in_call_pre"),
-        snapshot_total=Int("snapshot_total_pre"),
-        snapshot_sum_bal=Int("snapshot_sum_bal_pre"),
-        reserveX=Int("reserveX_pre"), reserveY=Int("reserveY_pre"),
-        lpSupply=Int("lpSupply_pre"),
-        lpBal=Array("lpBal_pre", IntSort(), IntSort()),
-        sumLpBal=Int("sumLpBal_pre"), initialK=Int("initialK_pre"),
-        collateral=Array("collateral_pre", IntSort(), IntSort()),
-        debt=Array("debt_pre", IntSort(), IntSort()),
-        totalCollateral=Int("totalCollateral_pre"), totalDebt=Int("totalDebt_pre"),
-        sumCollateral=Int("sumCollateral_pre"), sumDebt=Int("sumDebt_pre"),
-        liqThreshold=Int("liqThreshold_pre"),
-        staked=Array("staked_pre", IntSort(), IntSort()),
-        rewards_arr=Array("rewards_pre", IntSort(), IntSort()),
-        totalStaked=Int("totalStaked_pre"), sumStaked=Int("sumStaked_pre"),
-        rewardPool=Int("rewardPool_pre"), sumRewards=Int("sumRewards_pre"),
-        cross_in_progress=Int("cross_in_progress_pre"),
-        cross_snapshot_total=Int("cross_snapshot_total_pre"),
-        cross_snapshot_sum_bal=Int("cross_snapshot_sum_bal_pre"),
-        price=Int("price_pre"), twap_age=Int("twap_age_pre"),
-        timelock_time=Int("timelock_time_pre"),
+        Int(f"totalAssets_{sfx}"), Int(f"totalShares_{sfx}"),
+        Array(f"balances_{sfx}", IntSort(), IntSort()),
+        Array(f"shares_{sfx}", IntSort(), IntSort()),
+        Array(f"allowances_{sfx}", IntSort(), IntSort()),
+        Int(f"sumBalances_{sfx}"), Int(f"sumShares_{sfx}"),
+        locks=Array(f"locks_{sfx}", IntSort(), IntSort()),
+        in_call=Int(f"in_call_{sfx}"),
+        snapshot_total=Int(f"snapshot_total_{sfx}"),
+        snapshot_sum_bal=Int(f"snapshot_sum_bal_{sfx}"),
+        reserveX=Int(f"reserveX_{sfx}"), reserveY=Int(f"reserveY_{sfx}"),
+        lpSupply=Int(f"lpSupply_{sfx}"),
+        lpBal=Array(f"lpBal_{sfx}", IntSort(), IntSort()),
+        sumLpBal=Int(f"sumLpBal_{sfx}"), initialK=Int(f"initialK_{sfx}"),
+        collateral=Array(f"collateral_{sfx}", IntSort(), IntSort()),
+        debt=Array(f"debt_{sfx}", IntSort(), IntSort()),
+        totalCollateral=Int(f"totalCollateral_{sfx}"), totalDebt=Int(f"totalDebt_{sfx}"),
+        sumCollateral=Int(f"sumCollateral_{sfx}"), sumDebt=Int(f"sumDebt_{sfx}"),
+        liqThreshold=Int(f"liqThreshold_{sfx}"),
+        staked=Array(f"staked_{sfx}", IntSort(), IntSort()),
+        rewards_arr=Array(f"rewards_{sfx}", IntSort(), IntSort()),
+        totalStaked=Int(f"totalStaked_{sfx}"), sumStaked=Int(f"sumStaked_{sfx}"),
+        rewardPool=Int(f"rewardPool_{sfx}"), sumRewards=Int(f"sumRewards_{sfx}"),
+        cross_in_progress=Int(f"cross_in_progress_{sfx}"),
+        cross_snapshot_total=Int(f"cross_snapshot_total_{sfx}"),
+        cross_snapshot_sum_bal=Int(f"cross_snapshot_sum_bal_{sfx}"),
+        price=Int(f"price_{sfx}"), twap_age=Int(f"twap_age_{sfx}"),
+        timelock_time=Int(f"timelock_time_{sfx}"),
     )
 
 
-def _build_base_axioms(pre, invariants, touched, model):
+def _build_base_axioms(pre, invariants, touched, model, assume_invariants=True):
     base = []
-    for hyp in invariants:
-        base.append(_hypothesis(hyp, pre))
+    if assume_invariants:
+        for hyp in invariants:
+            base.append(_hypothesis(hyp, pre))
     u = Int("u")
@@ -642,1 +645,204 @@ base.append(Implies(ForAll([u], Select(pre.bal, u) >= 0),
     return s.check() == unsat
+
+
+# ── Init predicates + k-induction ───────────────────────────────────────
+#
+# Opt-in per binding:
+#     "init": ["all_zero"], "induction": {"k": 2}
+#
+# Base case (BMC): from init, for each depth 0..k-1, prove the invariant
+# holds — this discharges the initiation obligation that plain 1-induction
+# skips. A base violation is a REAL, reachable counterexample (stronger
+# evidence than a 1-induction step counterexample, whose pre-state may be
+# unreachable).
+#
+# Step: assuming ALL selected invariants hold at k consecutive states linked
+# by ANY function (the transition relation is the disjunction over all
+# functions — intermediate steps may use different functions), prove the
+# invariant at state k. Default k=1 is exactly the legacy engine.
+
+INIT_PREDS = {"all_zero"}
+
+
+def _apply_init(init_names, s):
+    """Constraints for a freshly-deployed state. all_zero zeroes all
+    accounting state (scalars, arrays, ghosts, locks) but leaves config
+    params (liqThreshold, initialK) free — they are constrained by the
+    model's base axioms instead."""
+    conds = []
+    for name in init_names:
+        name = name.strip()
+        if name != "all_zero":
+            raise ValueError(f"unknown init predicate: {name}")
+        # Constant-array equality (arr == K(0)) is quantifier-free and far
+        # cheaper than ForAll u. Select(arr, u) == 0.
+        z = K(IntSort(), IntVal(0))
+        conds.extend([
+            s.total == 0, s.total_shares == 0, s.sum_bal == 0, s.sum_shr == 0,
+            s.in_call == 0, s.snapshot_total == 0, s.snapshot_sum_bal == 0,
+            s.reserveX == 0, s.reserveY == 0, s.lpSupply == 0, s.sumLpBal == 0,
+            s.totalCollateral == 0, s.totalDebt == 0,
+            s.sumCollateral == 0, s.sumDebt == 0,
+            s.totalStaked == 0, s.sumStaked == 0,
+            s.rewardPool == 0, s.sumRewards == 0,
+            s.cross_in_progress == 0,
+            s.cross_snapshot_total == 0, s.cross_snapshot_sum_bal == 0,
+            s.price == 0, s.twap_age == 0, s.timelock_time == 0,
+            s.bal == z, s.shr == z, s.allow == z, s.locks == z,
+            s.lpBal == z, s.collateral == z, s.debt_arr == z,
+            s.staked == z, s.rewards_arr == z,
+        ])
+    return conds
+
+
+def _state_eq(a, b):
+    return [
+        a.total == b.total, a.total_shares == b.total_shares,
+        a.bal == b.bal, a.shr == b.shr, a.allow == b.allow,
+        a.sum_bal == b.sum_bal, a.sum_shr == b.sum_shr,
+        a.locks == b.locks, a.in_call == b.in_call,
+        a.snapshot_total == b.snapshot_total, a.snapshot_sum_bal == b.snapshot_sum_bal,
+        a.reserveX == b.reserveX, a.reserveY == b.reserveY,
+        a.lpSupply == b.lpSupply, a.lpBal == b.lpBal,
+        a.sumLpBal == b.sumLpBal, a.initialK == b.initialK,
+        a.collateral == b.collateral, a.debt_arr == b.debt_arr,
+        a.totalCollateral == b.totalCollateral, a.totalDebt == b.totalDebt,
+        a.sumCollateral == b.sumCollateral, a.sumDebt == b.sumDebt,
+        a.liqThreshold == b.liqThreshold,
+        a.staked == b.staked, a.rewards_arr == b.rewards_arr,
+        a.totalStaked == b.totalStaked, a.sumStaked == b.sumStaked,
+        a.rewardPool == b.rewardPool, a.sumRewards == b.sumRewards,
+        a.cross_in_progress == b.cross_in_progress,
+        a.cross_snapshot_total == b.cross_snapshot_total,
+        a.cross_snapshot_sum_bal == b.cross_snapshot_sum_bal,
+        a.price == b.price, a.twap_age == b.twap_age,
+        a.timelock_time == b.timelock_time,
+    ]
+
+
+def _link(funcs, sj, sj1, link_id):
+    """One transition step sj -> sj1 taken by ANY function in the binding.
+    Returns (constraint, touched, callvars)."""
+    actor, to, src, owner = (Int(f"actor_{link_id}"), Int(f"to_{link_id}"),
+                             Int(f"src_{link_id}"), Int(f"owner_{link_id}"))
+    amt, dy = Int(f"amt_{link_id}"), Int(f"dy_{link_id}")
+    domain = [actor >= 0, to >= 0, src >= 0, owner >= 0]
+    branches = []
+    for func in funcs:
+        fid = IntVal(func.get("func_id", 0))
+        guards = _apply_guards(func["guards"], sj, actor, to, src, owner, amt,
+                               fid, dy=dy)
+        post = _apply_effects(func["effects"], sj, actor, to, src, amt,
+                              fid, dy=dy)
+        branches.append(And(*(guards + _state_eq(post, sj1))))
+    cvars = {"actor": actor, "to": to, "src": src, "owner": owner,
+             "amt": amt, "dy": dy}
+    return And(Or(*branches), *domain), [actor, to, src], cvars
+
+
+def _extract_cex(m, pre, post, cvars):
+    ev = lambda t: str(m.eval(t, model_completion=True))
+    cex = {}
+    if cvars:
+        cex.update({
+            "actor": ev(cvars["actor"]), "to": ev(cvars["to"]),
+            "src": ev(cvars["src"]), "amt": ev(cvars["amt"]),
+            "dy": ev(cvars["dy"]),
+        })
+    else:
+        cex.update({"actor": "-", "to": "-", "src": "-", "amt": "-", "dy": "-"})
+    cex.update({
+        "totalAssets_pre": ev(pre.total), "totalAssets_post": ev(post.total),
+        "totalShares_pre": ev(pre.total_shares), "totalShares_post": ev(post.total_shares),
+        "sumBalances_pre": ev(pre.sum_bal), "sumBalances_post": ev(post.sum_bal),
+        "reserveX_pre": ev(pre.reserveX), "reserveX_post": ev(post.reserveX),
+        "totalCollateral_pre": ev(pre.totalCollateral),
+        "totalCollateral_post": ev(post.totalCollateral),
+        "totalDebt_pre": ev(pre.totalDebt), "totalDebt_post": ev(post.totalDebt),
+    })
+    if cvars:
+        cex["balance_actor_pre"] = ev(Select(pre.bal, cvars["actor"]))
+        cex["balance_actor_post"] = ev(Select(post.bal, cvars["actor"]))
+    return cex
+
+
+def check_k_induction(funcs, invariants, model, init_names, k):
+    """k-induction over the whole transition relation. Returns per-invariant
+    results: base (BMC from init, depths 0..k-1) then step (k-linked)."""
+    states = [_build_pre_state(model, sfx=f"s{i}") for i in range(k + 1)]
+    links, touched_per_link, cvars_per_link = [], [], []
+    for i in range(k):
+        c, touched, cvars = _link(funcs, states[i], states[i + 1], i)
+        links.append(c)
+        touched_per_link.append(touched)
+        cvars_per_link.append(cvars)
+
+    results = []
+    for inv in invariants:
+        # ── Base case: invariant holds at depths 0..k-1 from init ──
+        base_violation = None
+        base_unknown = False
+        for d in range(0, k):
+            s = Solver()
+            s.set("timeout", 30000)
+            s.add(_apply_init(init_names, states[0]))
+            s.add(_build_base_axioms(states[0], [], [], model,
+                                     assume_invariants=False))
+            for i in range(d):
+                s.add(links[i])
+                s.add(_build_base_axioms(states[i + 1], [], touched_per_link[i],
+                                         model, assume_invariants=False))
+            s.add(Not(_hypothesis(inv, states[d])))
+            r = s.check()
+            if r == sat:
+                m = s.model()
+                cvars = cvars_per_link[d - 1] if d > 0 else None
+                base_violation = {
+                    "depth": d,
+                    "cex": _extract_cex(m, states[max(d - 1, 0)], states[d], cvars),
+                }
+                break
+            elif r != unsat:
+                base_unknown = True
+                break
+
+        if base_violation is not None:
+            results.append({
+                "invariant": inv, "status": "violated",
+                "counterexample": base_violation["cex"],
+                "base": {"violated_at_depth": base_violation["depth"]},
+                "step": "skipped",
+            })
+            continue
+        if base_unknown:
+            results.append({"invariant": inv, "status": "unknown",
+                            "counterexample": None, "base": "unknown",
+                            "step": "skipped"})
+            continue
+
+        # ── Step: inv(s0..s_{k-1}) ∧ links ⟹ inv(s_k) ──
+        s = Solver()
+        s.set("timeout", 30000)
+        for i in range(k):
+            s.add(_build_base_axioms(states[i], invariants, touched_per_link[i],
+                                     model, assume_invariants=True))
+            s.add(links[i])
+        s.add(Not(_goal(inv, states[k], touched_per_link[k - 1], model)))
+        r = s.check()
+        if r == unsat:
+            results.append({"invariant": inv, "status": "proved",
+                            "counterexample": None, "base": "held",
+                            "step": "passed"})
+        elif r == sat:
+            m = s.model()
+            results.append({
+                "invariant": inv, "status": "violated",
+                "counterexample": _extract_cex(m, states[k - 1], states[k],
+                                               cvars_per_link[k - 1]),
+                "base": "held", "step": "failed",
+            })
+        else:
+            results.append({"invariant": inv, "status": "unknown",
+                            "counterexample": None, "base": "held",
+                            "step": "unknown"})
+    return {"invariants": results}

src/cli.js

@@ -57,2 +57,4 @@ #!/usr/bin/env node
   bytecode       Halmos symbolic execution against EVM bytecode.
+                 Add --expect to gate on halmos/expectations.json (safe must PASS,
+                 known exploits must FAIL with a counterexample). Exit 0 iff all match.
   bench          Run all benchmark + defihack cases.
@@ -143,3 +145,8 @@ audit          Verify the tamper-evident audit chain.
   if (cmd === 'bytecode') {
-    const testGlob = process.argv[3] || '*';
+    if (process.argv.includes('--expect')) {
+      const { spawnSync } = require('child_process');
+      const r = spawnSync(process.execPath, [path.join(__dirname, '..', 'bench', 'halmos-check.js')], { stdio: 'inherit' });
+      process.exit(r.status == null ? 2 : r.status);
+    }
+    const testGlob = (process.argv[3] && !process.argv[3].startsWith('--')) ? process.argv[3] : '*';
     const res = runHalmos(testGlob);
@@ -482,5 +489,14 @@ if (!res.ok) { console.error(`halmos error: ${res.error}`); process.exit(2); }
 
+    server.on('error', (e) => {
+      const msg = e.code === 'EADDRINUSE'
+        ? `port ${port} already in use (try --port 0 for an OS-assigned port)`
+        : e.message;
+      console.error(`${C.red}serve error:${C.reset} ${msg}`);
+      process.exit(2);
+    });
+
     server.listen(port, () => {
-      console.log(`${C.green}Dashboard:${C.reset} http://localhost:${port}`);
-      console.log(`${C.green}Badge:${C.reset}    http://localhost:${port}/badge.svg`);
+      const actualPort = server.address().port;
+      console.log(`${C.green}Dashboard:${C.reset} http://localhost:${actualPort}`);
+      console.log(`${C.green}Badge:${C.reset}    http://localhost:${actualPort}/badge.svg`);
       console.log(`\n${C.dim}Press Ctrl+C to stop${C.reset}`);
@@ -487,0 +503,0 @@ });

src/halmos-runner.js

@@ -79,2 +79,7 @@ const { spawnSync } = require('child_process');
 function runHalmos(testGlob) {
+  // '*' (or empty) means "all test contracts" — halmos's --contract filter is a
+  // regex, so a literal '*' is an invalid pattern and yields zero results.
+  // Omit the flag entirely instead (also picks up future test contracts).
+  const contractArgs = (testGlob && testGlob !== '*') ? ['--contract', testGlob] : [];
+
   const halmosBin = pickHalmos();
@@ -87,3 +92,3 @@ if (halmosBin) {
 
-    const res = spawnSync(halmosBin, ['--root', HALMOS_DIR, '--contract', testGlob], {
+    const res = spawnSync(halmosBin, ['--root', HALMOS_DIR, ...contractArgs], {
       cwd: HALMOS_DIR,
@@ -107,3 +112,3 @@ encoding: 'utf-8',
 
-    const res = spawnSync(python, ['-m', 'halmos', '--root', HALMOS_DIR, '--contract', testGlob], {
+    const res = spawnSync(python, ['-m', 'halmos', '--root', HALMOS_DIR, ...contractArgs], {
       cwd: HALMOS_DIR,
@@ -128,3 +133,5 @@ encoding: 'utf-8',
   const lines = clean.split('\n');
-  let currentFail = null;
+  // halmos prints the counterexample block BEFORE the [FAIL] summary line,
+  // so buffer cex vars and attach them to the next [FAIL] (cleared on [PASS]).
+  let pendingCex = {};
 
@@ -137,8 +144,9 @@ for (const line of lines) {
       results.push({ name: passMatch[1], passed: true, counterexample: null });
-      currentFail = null;
+      pendingCex = {};
     } else if (failMatch) {
-      currentFail = { name: failMatch[1], passed: false, counterexample: {} };
-      results.push(currentFail);
+      results.push({ name: failMatch[1], passed: false, counterexample: pendingCex });
+      pendingCex = {};
     } else if (line.includes('Counterexample')) {
-    } else if (currentFail && line.trim()) {
+      // header line — variable assignments follow
+    } else if (line.trim()) {
       const stripped = line.trim();
@@ -149,3 +157,3 @@ const eq = stripped.indexOf(' = ');
         const val = stripped.substring(eq + 3).trim();
-        currentFail.counterexample[key] = val;
+        pendingCex[key] = val;
       }
@@ -152,0 +160,0 @@ }

src/report.js

@@ -55,4 +55,25 @@ const C = {
     (result.llmUsage ? ` (${result.llmUsage.provider}/${result.llmUsage.model}, ${result.llmUsage.inputTokens}+${result.llmUsage.outputTokens} tok)` : ''));
+  if (result.solver.proof) {
+    const p = result.solver.proof;
+    lines.push(`${C.dim}proof:${C.reset} ${p.kind === 'k-induction' ? `k-induction (k=${p.k}, init: ${(p.init || []).join(', ')})` : '1-induction'}`);
+  }
   lines.push('');
 
+  if (Array.isArray(result.solver.invariants)) {
+    for (const r of result.solver.invariants) {
+      if (r.status === 'proved') {
+        lines.push(`    ${C.green}✓ proved${C.reset}   ${r.invariant} ${C.dim}(base held, step passed)${C.reset}`);
+      } else if (r.status === 'violated') {
+        const where = r.base && r.base.violated_at_depth !== undefined
+          ? `base case, depth ${r.base.violated_at_depth} (reachable from init)`
+          : 'inductive step';
+        lines.push(`    ${C.red}✗ violated${C.reset} ${r.invariant} ${C.dim}— ${where}${C.reset}`);
+        lines.push(...renderCex(r.counterexample));
+      } else {
+        lines.push(`    ${C.yellow}? unknown${C.reset}  ${r.invariant}`);
+      }
+    }
+    lines.push('');
+  }
+
   for (const fn of result.solver.functions) {
@@ -63,3 +84,3 @@ lines.push(`  ${C.cyan}${C.bold}${fn.function}()${C.reset}`);
     }
-    for (const r of fn.results) {
+    for (const r of fn.results || []) {
       if (r.status === 'proved') {
@@ -66,0 +87,0 @@ lines.push(`    ${C.green}✓ proved${C.reset}   ${r.invariant}`);

New alerts

AI-detected potential code anomaly

Supply chain risk

AI has identified unusual behaviors that may pose a security risk.

Long strings

Supply chain risk

Contains long string literals, which may be a sign of obfuscated or packed code.

URL strings

Supply chain risk

Package contains fragments of external URLs or IP addresses, which the package may be accessing at runtime.

Fixed alerts

Long strings

Supply chain risk

Contains long string literals, which may be a sign of obfuscated or packed code.

URL strings

Supply chain risk

Package contains fragments of external URLs or IP addresses, which the package may be accessing at runtime.

Improved metrics

Total package byte prevSize

2983427

0.74%

Number of package files

105

2.94%

Lines of code

5003

8.5%

Number of lines in readme file

138

4.55%

Worsened metrics

Number of low supply chain risk alerts

33

6.45%

Number of medium supply chain risk alerts

14

7.69%

No dependency changes