v0.4.0

One trace follows one path; this release proves the rest.

Highlights

• explore() and covers(): each traced branch condition is negated and handed to Z3, which produces an input for the other side or proves none exists. Coverage is claimed only when the solver proves the OR of path conditions covers the domain.
• @specifies checks every branch by default. A spec right on the tested branch and wrong on another now fails, with the guilty branch printed. A green test cannot hide an unchecked branch.
• @specifies.property: check a fact (entries sum to one, a null space holds) on every branch, with the failing input returned; inequalities checked by entailment.
• assume= simplification makes derivation-domain specs like the spline penalty closed forms checkable (#48, @be-student).
• FFT family joins the dialect: the DFT is a closed form at any n, so fft/ifft/rfft emit Sums; Parseval and linearity become provable, complex formulas are first class.
• Soundness: coverage completeness is a proven theorem, not bookkeeping; three CI oracles (ground-truth fuzzing, sympy-vs-Z3 differential, empirical coverage audit).
• z3-solver is now required (a plain pip wheel).
• New DESIGN.md (#40, @AAYUSHRAJPUT846) and branch_coverage_check.ipynb.

Measured: 274 of 293 public numpy functions that trace get full branch coverage proven.

pip install scikit-verify