Skip to content

v0.8.4 — whole-project verify

Choose a tag to compare

@tiagoschmitt tiagoschmitt released this 17 Aug 03:16
· 24 commits to main since this release

One command, whole project:

theorem verify          # sweeps the project from the cwd, honoring theorem.config.ts
theorem verify src      # or any directory

Above ~12 files the CLI becomes an orchestrator: the contract registry is built from every file first — so cross-file call-site checks span the project instead of whatever happened to share a batch — then chunks of 6 files are verified in child processes, each with a fresh Z3 WASM heap (the heap degrades past ~15-20 files in one process; previously an invalid argument crash users had to work around with xargs). Children stream per-file output; the parent prints one grand total and reports, rather than dies with, a crashed shard.

Total  40 proved · 55 failed  (44 files with contracts of 338 scanned)

Also: Math.round(x) is modeled exactly as to_int(x + 0.5) — JS half-up semantics including negative halves — closing a silent body-drop where any function returning Math.round(...) verified against a free result (counterexamples showed impossible values like result = -1 for a sum of non-negatives).

~320 core tests.