diff --git a/.gitignore b/.gitignore
index 7b54abd..0a9d932 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,7 @@
 LOCAL.md
 .env
 .coherence/
+.hegel/
 .claude/ralph-loop.local.md
 bin/
 .chant/
diff --git a/README.md b/README.md
index 77d0858..61332e5 100644
--- a/README.md
+++ b/README.md
@@ -332,7 +332,7 @@ chant init [--force] [--json]       # scaffold chant.yml, recipes/, skill, gitig
 chant index [--no-registry] [--json]   # rebuild .chant/index.json (+ upsert into the per-machine registry)
 chant status [--json]               # rewrite .chant/STATUS.md
 chant doctor [--json]               # validate config + store
-chant bench [--suite=retrieval|e2e|all] [--json]   # run the validation suite
+chant bench [--suite=retrieval|e2e|properties|all] [--json]   # run the validation suite
 chant version
 chant help
 ```
@@ -532,17 +532,24 @@ go test ./...
 ## Bench
 
 `chant bench` runs the shipped validation suites and exits 1 on any failure —
-same CI muscle memory as `coherence bench`:
+same CI muscle memory as `coherence bench`. The default `all` suite is the
+fast gate (`retrieval` + `e2e`); Hegel properties are opt-in:
 
 ```bash
 chant bench                      # default: all suites
 chant bench --suite=retrieval    # retrieval ranking scenarios (incl. true negatives)
 chant bench --suite=e2e          # run + verify every recipe with an example, asserting the trust gate
+chant bench --suite=properties   # Hegel property tests; starts hegel-core
 chant bench --json               # machine-readable
 ```
 
 The retrieval suite asserts which recipe ranks first for a query (and that an
 unrelated query yields **no** match). The e2e suite proves the verifier-first
 gate end to end: each recipe with a verifier and an example is run and verified,
-and is only counted as a pass when the verifier establishes trust. See
+and is only counted as a pass when the verifier establishes trust. The
+properties suite uses Hegel under the `hegel` build tag to generate cases for
+retrieval, runner, spell-hash, and CSV recipe invariants; Hegel state is kept
+under `.chant/hegel/`, with the latest report at
+`.chant/hegel/properties-report.json` and failure payloads under
+`.chant/hegel/failures/`. See
 [`internal/bench/bench.go`](internal/bench/bench.go).
diff --git a/cmd/chant/commands.go b/cmd/chant/commands.go
index e9bf85f..168ded5 100644
--- a/cmd/chant/commands.go
+++ b/cmd/chant/commands.go
@@ -1177,7 +1177,7 @@ func cmdDoctor(args []string) error {
 
 func cmdBench(args []string) error {
 	fs := flag.NewFlagSet("bench", flag.ContinueOnError)
-	suite := fs.String("suite", "all", "retrieval | e2e | all")
+	suite := fs.String("suite", "all", "retrieval | e2e | properties | all")
 	asJSON := fs.Bool("json", false, "emit JSON")
 	if err := fs.Parse(args); err != nil {
 		return err
@@ -1187,15 +1187,27 @@ func cmdBench(args []string) error {
 		return err
 	}
 	var summaries []bench.Summary
-	if *suite == "retrieval" || *suite == "all" {
+	switch *suite {
+	case "retrieval":
+		summaries = append(summaries, bench.RunRetrieval(s.Config.Retrieval))
+	case "e2e":
+		e2e, err := bench.RunE2E(s)
+		if err != nil {
+			return err
+		}
+		summaries = append(summaries, e2e)
+	case "properties":
+		summaries = append(summaries, bench.RunProperties(s.Root))
+	case "all":
+		// Keep all as the fast, backward-compatible gate: retrieval + e2e.
 		summaries = append(summaries, bench.RunRetrieval(s.Config.Retrieval))
-	}
-	if *suite == "e2e" || *suite == "all" {
 		e2e, err := bench.RunE2E(s)
 		if err != nil {
 			return err
 		}
 		summaries = append(summaries, e2e)
+	default:
+		return fmt.Errorf("unknown bench suite %q (want retrieval, e2e, properties, or all)", *suite)
 	}
 	failed := 0
 	for _, sum := range summaries {
diff --git a/cmd/chant/main.go b/cmd/chant/main.go
index 60b0434..2e47b1c 100644
--- a/cmd/chant/main.go
+++ b/cmd/chant/main.go
@@ -121,7 +121,7 @@ Repo:
   index    [--no-registry]   rebuild .chant/index.json (and upsert into the per-machine registry)
   status                     rewrite .chant/STATUS.md
   doctor                     validate config + store
-  bench [--suite=retrieval|e2e|all]   run the validation suite
+  bench [--suite=retrieval|e2e|properties|all]   run the validation suite
   version
 
 Most commands accept --json for a stable machine-readable outcome contract.
diff --git a/cmd/chant/main_test.go b/cmd/chant/main_test.go
index 62a658b..382f0cc 100644
--- a/cmd/chant/main_test.go
+++ b/cmd/chant/main_test.go
@@ -304,6 +304,26 @@ func TestCLI_JSONErrorEmitsBlockingError(t *testing.T) {
 	}
 }
 
+func TestCLI_BenchUnknownSuiteJSONError(t *testing.T) {
+	bin := buildBinary(t)
+	repo := newRepo(t)
+	out, code := run(t, bin, repo, "bench", "--suite=bogus", "--json")
+	if code != 1 {
+		t.Errorf("expected exit 1 for unknown bench suite, got %d\n%s", code, out)
+	}
+	var e struct {
+		BlockingError bool   `json:"blocking_error"`
+		Message       string `json:"message"`
+		Subcommand    string `json:"subcommand"`
+	}
+	if err := json.Unmarshal([]byte(out), &e); err != nil {
+		t.Fatalf("bench error path did not emit JSON under --json: %v\n%s", err, out)
+	}
+	if !e.BlockingError || e.Subcommand != "bench" || !strings.Contains(e.Message, "unknown bench suite") {
+		t.Errorf("unexpected bench error JSON: %+v\n%s", e, out)
+	}
+}
+
 // TestCLI_SuggestEmptyLibraryMatchFound verifies match_found is always present
 // (false), even with no recipes, so agents can gate on it unconditionally.
 func TestCLI_SuggestEmptyLibraryMatchFound(t *testing.T) {
diff --git a/docs/README.md b/docs/README.md
index 1704f5a..2f27dc9 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -23,6 +23,7 @@ A chant recipe is also called an **enchantment** (synonym; the on-disk form is
 docs/
 ├── README.md            ← you are here
 ├── commands/            ← one page per CLI command
+├── integration/         ← integration notes such as Hegel
 └── specs/               ← design specs (owned by the lead; see enchantment-metadata.md)
 ```
 
@@ -129,16 +130,22 @@ graph edges. The canonical design is
 
 ## Bench
 
-Every page's behavior is exercised by `chant bench`, which ships two suites:
+Every page's behavior is exercised by `chant bench`. The default `all` suite
+runs the two fast compatibility suites:
 
 - **retrieval** — synthetic recipe set + queries asserting which recipe ranks
   first (including true negatives: an unrelated query must NOT match).
 - **e2e** — runs each recipe's procedure + verifier and asserts the
   verifier-first gate (trusted only after the verifier passes).
+- **properties** — opt-in Hegel property tests for retrieval, runner,
+  spell-hash, and CSV recipe invariants, with per-property case counts and
+  `.chant/hegel/` evidence files.
 
 ```bash
 chant bench --suite=all
+chant bench --suite=properties
 ```
 
 Exit code is `1` when any scenario fails — same CI muscle memory as
-`coherence bench`. See [`commands/bench.md`](commands/bench.md).
+`coherence bench`. See [`commands/bench.md`](commands/bench.md) and
+[`integration/hegel.md`](integration/hegel.md).
diff --git a/docs/commands/bench.md b/docs/commands/bench.md
index 8a46617..d67201c 100644
--- a/docs/commands/bench.md
+++ b/docs/commands/bench.md
@@ -7,8 +7,9 @@
 ## What it does
 
 Runs chant's shipped validation suites and exits `1` on any scenario failure —
-the same CI muscle memory as `coherence bench`. Two suites prove the core
-thesis:
+the same CI muscle memory as `coherence bench`. The default `all` suite is the
+fast compatibility gate: `retrieval` + `e2e`. The Hegel-backed `properties`
+suite is opt-in because it starts the Hegel runtime.
 
 - **`retrieval`** — a synthetic recipe set + queries, asserting which recipe
   ranks first and whether it clears the match threshold. Includes a **true
@@ -18,12 +19,18 @@ thesis:
   verifier establishes trust). Recipes without a verifier or without an example
   are skipped (reported as a pass with a skip note) so the suite stays green on
   a fresh library.
+- **`properties`** — runs build-tagged Hegel property tests for retrieval,
+  runner trust, spell hashes, and the CSV recipe oracle. Results are reported
+  per property with a `cases` count, and `.chant/hegel/properties-report.json`
+  preserves the latest report. On failure, generated-case evidence is written
+  under `.chant/hegel/failures/`. The suite may use Python/`uv` to start
+  `hegel-core` unless `HEGEL_SERVER_COMMAND` is set.
 
 ## Flags
 
 | Flag | Default | Meaning |
 |---|---|---|
-| `--suite` | `all` | `retrieval`, `e2e`, or `all`. |
+| `--suite` | `all` | `retrieval`, `e2e`, `properties`, or `all`. `all` intentionally excludes `properties`. |
 | `--json` | false | emit the suite summaries as JSON. |
 
 ## Example (human)
@@ -89,8 +96,36 @@ chant bench --json
 
 A top-level `{summaries[], failed}`. Each `Summary` carries `suite`, `total`,
 `passed`, `failed`, and `results[]`; each `Result` carries `id`, `name`,
-`suite`, `pass`, and a `detail` string. `failed` is the total failed across all
-suites; a non-zero value makes `chant bench` exit `1`.
+`suite`, `pass`, and a `detail` string. Property results may also carry
+`cases` and `failure_artifact`. `failed` is the total failed across all suites;
+a non-zero value makes `chant bench` exit `1`.
+
+The opt-in property suite has the same top-level JSON shape:
+
+```bash
+chant bench --suite=properties --json
+```
+
+```json
+{
+  "failed": 0,
+  "summaries": [
+    {
+      "suite": "properties",
+      "total": 5,
+      "passed": 5,
+      "failed": 0,
+      "results": [
+        {"id": "PROP-retrieval-stale-penalty", "name": "retrieval stale penalty", "suite": "properties", "pass": true, "detail": "Hegel property passed", "cases": 50},
+        {"id": "PROP-retrieval-signal-monotonicity", "name": "retrieval signal monotonicity", "suite": "properties", "pass": true, "detail": "Hegel property passed", "cases": 50},
+        {"id": "PROP-runner-trust-gate", "name": "runner trust gate", "suite": "properties", "pass": true, "detail": "Hegel property passed", "cases": 50},
+        {"id": "PROP-spell-hash-stability", "name": "spell hash stability", "suite": "properties", "pass": true, "detail": "Hegel property passed", "cases": 50},
+        {"id": "PROP-csv-recipe-oracle", "name": "CSV recipe oracle", "suite": "properties", "pass": true, "detail": "Hegel property passed", "cases": 25}
+      ]
+    }
+  ]
+}
+```
 
 ## What the scenarios assert
 
@@ -101,3 +136,8 @@ suites; a non-zero value makes `chant bench` exit `1`.
 | `RET-003` | a chargeback/refund task routes to `refund-chargeback-threat`. |
 | `RET-004` | column signals disambiguate revenue from a normalize recipe. |
 | `E2E-<id>` | each recipe with a verifier + example runs and verifies, and is trusted only on a passing verifier. |
+| `PROP-retrieval-stale-penalty` | Hegel generates cases proving stale recipes score exactly half and carry a stale warning. |
+| `PROP-retrieval-signal-monotonicity` | Hegel generates matching and unsatisfied structural signals and checks score behavior. |
+| `PROP-runner-trust-gate` | Hegel generates verifier/artifact combinations and checks trust is granted only through the gate. |
+| `PROP-spell-hash-stability` | Hegel generates equivalent commands and column orderings and checks `spell_hash` stability. |
+| `PROP-csv-recipe-oracle` | Hegel generates CSV rows/aliases and compares the recipe output to an independent oracle. |
diff --git a/docs/integration/hegel.md b/docs/integration/hegel.md
new file mode 100644
index 0000000..69bd65f
--- /dev/null
+++ b/docs/integration/hegel.md
@@ -0,0 +1,90 @@
+# Hegel integration
+
+Hegel is chant's opt-in generative verifier layer. It does not add a new trust
+path: `chant verify` still trusts a recipe only when `verification.command`
+exits 0 and every expected artifact exists.
+
+## How it fits
+
+Use Hegel when a recipe or internal invariant depends on input-shape variation:
+schema aliases, edge-case values, stale status, artifact combinations, or
+portable identity. Hegel supplies generated cases and shrinking; chant supplies
+the recipe, command execution, and verifier-first trust gate.
+
+For a recipe, keep using the existing verifier field:
+
+```yaml
+verification:
+  command: go test ./property -run TestCSVRevenueProperty -count=1
+  expected_artifacts:
+    - property-report.json
+```
+
+The verifier command can run any Hegel client. In this Go repo, use
+`hegel.dev/go/hegel` and ordinary `go test`.
+
+## Built-in property suite
+
+chant ships an opt-in Hegel suite:
+
+```bash
+chant bench --suite=properties
+chant bench --suite=properties --json
+```
+
+The default `chant bench` / `chant bench --suite=all` path intentionally stays
+fast and does not run Hegel. The property suite runs build-tagged tests with:
+
+```bash
+go test -tags hegel ./internal/bench -run TestHegelProperties -count=1
+```
+
+`chant bench --suite=properties --json` reports each property separately,
+including its generated case count. It also writes the latest evidence summary
+to `.chant/hegel/properties-report.json`.
+
+The suite covers:
+
+- `PROP-retrieval-stale-penalty` — 50 cases.
+- `PROP-retrieval-signal-monotonicity` — 50 cases.
+- `PROP-runner-trust-gate` — 50 cases.
+- `PROP-spell-hash-stability` — 50 cases.
+- `PROP-csv-recipe-oracle` — 25 cases.
+
+On failure, the Hegel test writes the generated case payload to
+`.chant/hegel/failures/<property-id>.json`. Hegel's own shrunk failure output is
+still emitted through `go test`; the chant artifact preserves the generated
+case data that caused the property to fail.
+
+## Hermetic CI
+
+Keep Hegel opt-in. For CI, preinstall the matching `hegel-core` binary and wire
+the command explicitly rather than relying on runtime `uv` installation:
+
+```yaml
+- name: Hegel properties
+  run: chant bench --suite=properties --json
+  env:
+    HEGEL_SERVER_COMMAND: /path/to/preinstalled/hegel
+```
+
+## Runtime notes
+
+Hegel is currently beta, so chant pins the Go client version. Hegel starts a
+`hegel-core` server at runtime; by default the client uses Python/`uv` to fetch
+and run the compatible server. In hermetic CI, preinstall `hegel-core` and set:
+
+```bash
+export HEGEL_SERVER_COMMAND=/path/to/hegel
+```
+
+chant sets `CHANT_HEGEL_DIR` for the built-in suite so Hegel state lives under
+`.chant/hegel/`. `.hegel/` is also gitignored as a fallback for Hegel server
+logs.
+
+References:
+
+- [How Hegel works](https://hegel.dev/explanation/how-hegel-works)
+- [Installation reference](https://hegel.dev/reference/installation)
+- [Compatibility](https://hegel.dev/compatibility)
+- [hegel-go API](https://pkg.go.dev/hegel.dev/go/hegel)
diff --git a/go.mod b/go.mod
index 51eef52..c3a950c 100644
--- a/go.mod
+++ b/go.mod
@@ -2,4 +2,12 @@ module github.com/fireharp/chant
 
 go 1.26.3
 
-require gopkg.in/yaml.v3 v3.0.1 // indirect
+require (
+	gopkg.in/yaml.v3 v3.0.1
+	hegel.dev/go/hegel v0.5.3
+)
+
+require (
+	github.com/fxamacker/cbor/v2 v2.9.0 // indirect
+	github.com/x448/float16 v0.8.4 // indirect
+)
diff --git a/go.sum b/go.sum
index 4bc0337..a3ca3e0 100644
--- a/go.sum
+++ b/go.sum
@@ -1,3 +1,10 @@
+github.com/fxamacker/cbor/v2 v2.9.0 h1:NpKPmjDBgUfBms6tr6JZkTHtfFGcMKsw3eGcmD/sapM=
+github.com/fxamacker/cbor/v2 v2.9.0/go.mod h1:vM4b+DJCtHn+zz7h3FFp/hDAI9WNWCsZj23V5ytsSxQ=
+github.com/x448/float16 v0.8.4 h1:qLwI1I70+NjRFUR3zs1JPUCgaCXSh3SW62uAKT1mSBM=
+github.com/x448/float16 v0.8.4/go.mod h1:14CWIYCyZA/cWjXOioeEpHeN/83MdbZDRQHoFcYsOfg=
+gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405 h1:yhCVgyC4o1eVCa2tZl7eS0r+SDo693bJlVdllGtEeKM=
 gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
 gopkg.in/yaml.v3 v3.0.1 h1:fxVm/GzAzEWqLHuvctI91KS9hhNmmWOoWu0XTYJS7CA=
 gopkg.in/yaml.v3 v3.0.1/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM=
+hegel.dev/go/hegel v0.5.3 h1:qd3C6pbrwC1SJSVojbPxMPRbPKlFPbLQL7HTLcbFceE=
+hegel.dev/go/hegel v0.5.3/go.mod h1:Y0rTUM/9YtGOj0poljehZ92IWW0Fv2qf47oqZzhzrXE=
diff --git a/internal/bench/bench.go b/internal/bench/bench.go
index 6fe27c8..4930fd9 100644
--- a/internal/bench/bench.go
+++ b/internal/bench/bench.go
@@ -27,11 +27,13 @@ import (
 
 // Result is one scenario outcome.
 type Result struct {
-	ID     string `json:"id"`
-	Name   string `json:"name"`
-	Suite  string `json:"suite"`
-	Pass   bool   `json:"pass"`
-	Detail string `json:"detail"`
+	ID              string `json:"id"`
+	Name            string `json:"name"`
+	Suite           string `json:"suite"`
+	Pass            bool   `json:"pass"`
+	Detail          string `json:"detail"`
+	Cases           int    `json:"cases,omitempty"`
+	FailureArtifact string `json:"failure_artifact,omitempty"`
 }
 
 // Summary aggregates a bench run.
diff --git a/internal/bench/bench_test.go b/internal/bench/bench_test.go
index 78eba2f..e00d250 100644
--- a/internal/bench/bench_test.go
+++ b/internal/bench/bench_test.go
@@ -1,6 +1,9 @@
 package bench
 
 import (
+	"encoding/json"
+	"os"
+	"path/filepath"
 	"strings"
 	"testing"
 
@@ -150,3 +153,27 @@ func TestE2E_NegativeGates(t *testing.T) {
 		}
 	}
 }
+
+func TestRecordPropertyFailureWritesArtifact(t *testing.T) {
+	dir := t.TempDir()
+	path, err := recordPropertyFailure(dir, "PROP-demo", map[string]any{
+		"case": "minimal",
+	})
+	if err != nil {
+		t.Fatalf("recordPropertyFailure: %v", err)
+	}
+	if path != filepath.Join(dir, "PROP-demo.json") {
+		t.Errorf("artifact path = %q, want %q", path, filepath.Join(dir, "PROP-demo.json"))
+	}
+	b, err := os.ReadFile(path)
+	if err != nil {
+		t.Fatalf("read artifact: %v", err)
+	}
+	var got map[string]any
+	if err := json.Unmarshal(b, &got); err != nil {
+		t.Fatalf("artifact JSON parse: %v\n%s", err, b)
+	}
+	if got["property_id"] != "PROP-demo" || got["case"] != "minimal" || got["recorded_at"] == "" {
+		t.Errorf("unexpected artifact payload: %+v", got)
+	}
+}
diff --git a/internal/bench/properties.go b/internal/bench/properties.go
new file mode 100644
index 0000000..9600c38
--- /dev/null
+++ b/internal/bench/properties.go
@@ -0,0 +1,198 @@
+package bench
+
+import (
+	"bytes"
+	"context"
+	"encoding/json"
+	"fmt"
+	"os"
+	"os/exec"
+	"path/filepath"
+	"regexp"
+	"strings"
+	"time"
+)
+
+type PropertySpec struct {
+	ID       string
+	Name     string
+	TestName string
+	Cases    int
+}
+
+var propertySpecs = []PropertySpec{
+	{ID: "PROP-retrieval-stale-penalty", Name: "retrieval stale penalty", TestName: "PROP-retrieval-stale-penalty", Cases: 50},
+	{ID: "PROP-retrieval-signal-monotonicity", Name: "retrieval signal monotonicity", TestName: "PROP-retrieval-signal-monotonicity", Cases: 50},
+	{ID: "PROP-runner-trust-gate", Name: "runner trust gate", TestName: "PROP-runner-trust-gate", Cases: 50},
+	{ID: "PROP-spell-hash-stability", Name: "spell hash stability", TestName: "PROP-spell-hash-stability", Cases: 50},
+	{ID: "PROP-csv-recipe-oracle", Name: "CSV recipe oracle", TestName: "PROP-csv-recipe-oracle", Cases: 25},
+}
+
+func PropertySpecs() []PropertySpec {
+	return append([]PropertySpec(nil), propertySpecs...)
+}
+
+type propertyReport struct {
+	GeneratedAt string   `json:"generated_at"`
+	Suite       string   `json:"suite"`
+	Results     []Result `json:"results"`
+}
+
+// RunProperties runs the opt-in Hegel property suite. Hegel imports live behind
+// the "hegel" build tag; this wrapper keeps normal `go test ./...` and
+// `chant bench --suite=all` free of Hegel runtime startup.
+func RunProperties(root string) Summary {
+	sum := Summary{Suite: "properties"}
+
+	if root == "" {
+		var err error
+		root, err = os.Getwd()
+		if err != nil {
+			res := Result{
+				ID:     "PROP-setup",
+				Name:   "property suite setup",
+				Suite:  "properties",
+				Pass:   false,
+				Detail: "could not determine working directory: " + err.Error(),
+			}
+			record(&sum, res)
+			return sum
+		}
+	}
+
+	hegelRoot := filepath.Join(root, ".chant", "hegel")
+	hegelDir := filepath.Join(hegelRoot, ".hegel")
+	failureDir := filepath.Join(hegelRoot, "failures")
+	reportPath := filepath.Join(hegelRoot, "properties-report.json")
+	for _, dir := range []string{hegelDir, failureDir} {
+		if err := os.MkdirAll(dir, 0o755); err != nil {
+			res := Result{
+				ID:     "PROP-setup",
+				Name:   "property suite setup",
+				Suite:  "properties",
+				Pass:   false,
+				Detail: "could not create Hegel state dir: " + err.Error(),
+			}
+			record(&sum, res)
+			return sum
+		}
+	}
+
+	for _, spec := range propertySpecs {
+		record(&sum, runProperty(root, hegelDir, failureDir, spec))
+	}
+
+	report := propertyReport{
+		GeneratedAt: time.Now().UTC().Format(time.RFC3339),
+		Suite:       "properties",
+		Results:     sum.Results,
+	}
+	if err := writeJSON(reportPath, report); err != nil {
+		res := Result{
+			ID:     "PROP-report",
+			Name:   "property report",
+			Suite:  "properties",
+			Pass:   false,
+			Detail: "could not write property report: " + err.Error(),
+		}
+		record(&sum, res)
+	}
+	return sum
+}
+
+func runProperty(root, hegelDir, failureDir string, spec PropertySpec) Result {
+	res := Result{
+		ID:     spec.ID,
+		Name:   spec.Name,
+		Suite:  "properties",
+		Pass:   true,
+		Cases:  spec.Cases,
+		Detail: "Hegel property passed",
+	}
+
+	failurePath := filepath.Join(failureDir, spec.ID+".json")
+	_ = os.Remove(failurePath)
+	ctx, cancel := context.WithTimeout(context.Background(), 5*time.Minute)
+	defer cancel()
+
+	runPattern := fmt.Sprintf("^TestHegelProperties$/^%s$", regexp.QuoteMeta(spec.TestName))
+	cmd := exec.CommandContext(ctx, "go", "test", "-tags", "hegel", "./internal/bench", "-run", runPattern, "-count=1", "-v")
+	cmd.Dir = root
+	cmd.Env = append(os.Environ(),
+		"CHANT_REPO_ROOT="+root,
+		"CHANT_HEGEL_DIR="+hegelDir,
+		"CHANT_HEGEL_FAILURE_DIR="+failureDir,
+	)
+
+	var out bytes.Buffer
+	cmd.Stdout = &out
+	cmd.Stderr = &out
+	err := cmd.Run()
+	if ctx.Err() == context.DeadlineExceeded {
+		res.Pass = false
+		res.Detail = "Hegel property timed out after 5m"
+	} else if err != nil {
+		res.Pass = false
+		res.Detail = trimDetail(out.String())
+		if res.Detail == "" {
+			res.Detail = err.Error()
+		}
+	}
+	if !res.Pass {
+		if rel, ok := existingArtifact(root, failurePath); ok {
+			res.FailureArtifact = rel
+		}
+	}
+	return res
+}
+
+func writeJSON(path string, v any) error {
+	b, err := json.MarshalIndent(v, "", "  ")
+	if err != nil {
+		return err
+	}
+	b = append(b, '\n')
+	return os.WriteFile(path, b, 0o644)
+}
+
+func existingArtifact(root, path string) (string, bool) {
+	if _, err := os.Stat(path); err != nil {
+		return "", false
+	}
+	if rel, err := filepath.Rel(root, path); err == nil {
+		return rel, true
+	}
+	return path, true
+}
+
+func recordPropertyFailure(failureDir, propertyID string, payload map[string]any) (string, error) {
+	if failureDir == "" {
+		return "", nil
+	}
+	if err := os.MkdirAll(failureDir, 0o755); err != nil {
+		return "", err
+	}
+	record := make(map[string]any, len(payload)+2)
+	for k, v := range payload {
+		record[k] = v
+	}
+	record["property_id"] = propertyID
+	record["recorded_at"] = time.Now().UTC().Format(time.RFC3339)
+	path := filepath.Join(failureDir, propertyID+".json")
+	if err := writeJSON(path, record); err != nil {
+		return "", err
+	}
+	return path, nil
+}
+
+func trimDetail(s string) string {
+	lines := strings.Split(strings.TrimSpace(s), "\n")
+	if len(lines) == 0 {
+		return ""
+	}
+	const keep = 12
+	if len(lines) > keep {
+		lines = lines[len(lines)-keep:]
+	}
+	return strings.Join(lines, "\n")
+}
diff --git a/internal/bench/properties_hegel_test.go b/internal/bench/properties_hegel_test.go
new file mode 100644
index 0000000..dfa007f
--- /dev/null
+++ b/internal/bench/properties_hegel_test.go
@@ -0,0 +1,525 @@
+//go:build hegel
+
+package bench
+
+import (
+	"encoding/csv"
+	"encoding/json"
+	"fmt"
+	"math"
+	"os"
+	"os/exec"
+	"path/filepath"
+	"strconv"
+	"strings"
+	"testing"
+	"time"
+
+	"github.com/fireharp/chant/internal/config"
+	"github.com/fireharp/chant/internal/recipe"
+	"github.com/fireharp/chant/internal/retrieve"
+	"github.com/fireharp/chant/internal/runner"
+	"hegel.dev/go/hegel"
+)
+
+func TestRunProperties_AllPass(t *testing.T) {
+	sum := RunProperties(repoRoot(t))
+	if sum.Failed != 0 {
+		for _, r := range sum.Results {
+			if !r.Pass {
+				t.Errorf("%s failed: %s", r.ID, r.Detail)
+			}
+		}
+	}
+	if sum.Suite != "properties" || sum.Total != len(PropertySpecs()) {
+		t.Errorf("summary = %+v, want %d properties results", sum, len(PropertySpecs()))
+	}
+	for _, r := range sum.Results {
+		if r.Cases == 0 {
+			t.Errorf("%s has no case count: %+v", r.ID, r)
+		}
+	}
+}
+
+func TestHegelProperties(t *testing.T) {
+	setupHegel(t)
+
+	for _, spec := range PropertySpecs() {
+		spec := spec
+		t.Run(spec.TestName, func(t *testing.T) {
+			switch spec.ID {
+			case "PROP-retrieval-stale-penalty":
+				propRetrievalStalePenalty(t)
+			case "PROP-retrieval-signal-monotonicity":
+				propRetrievalSignalMonotonicity(t)
+			case "PROP-runner-trust-gate":
+				propRunnerTrustGate(t)
+			case "PROP-spell-hash-stability":
+				propSpellHashStability(t)
+			case "PROP-csv-recipe-oracle":
+				propCSVRecipeOracle(t)
+			default:
+				t.Fatalf("unknown property spec %s", spec.ID)
+			}
+		})
+	}
+}
+
+func setupHegel(t *testing.T) {
+	t.Helper()
+	dir := os.Getenv("CHANT_HEGEL_DIR")
+	if dir == "" {
+		dir = filepath.Join(repoRoot(t), ".chant", "hegel", ".hegel")
+	}
+	if err := os.MkdirAll(filepath.Join(dir, "db"), 0o755); err != nil {
+		t.Fatalf("create Hegel dir: %v", err)
+	}
+	failureDir := os.Getenv("CHANT_HEGEL_FAILURE_DIR")
+	if failureDir == "" {
+		failureDir = filepath.Join(filepath.Dir(dir), "failures")
+		if err := os.Setenv("CHANT_HEGEL_FAILURE_DIR", failureDir); err != nil {
+			t.Fatalf("set Hegel failure dir: %v", err)
+		}
+	}
+	if err := os.MkdirAll(failureDir, 0o755); err != nil {
+		t.Fatalf("create Hegel failure dir: %v", err)
+	}
+	hegel.SetHegelDirectory(dir)
+}
+
+func hegelOpts(t *testing.T, cases int) []hegel.Option {
+	t.Helper()
+	dir := os.Getenv("CHANT_HEGEL_DIR")
+	if dir == "" {
+		dir = filepath.Join(repoRoot(t), ".chant", "hegel", ".hegel")
+	}
+	db := filepath.Join(dir, "db")
+	if err := os.MkdirAll(db, 0o755); err != nil {
+		t.Fatalf("create Hegel db: %v", err)
+	}
+	return []hegel.Option{
+		hegel.WithTestCases(cases),
+		hegel.WithDatabase(hegel.Database(db)),
+		hegel.WithDerandomize(true),
+	}
+}
+
+func propRetrievalStalePenalty(t *testing.T) {
+	cfg := config.Default().Retrieval
+	tasks := []string{
+		"compute revenue by channel from csv",
+		"analyze ecommerce orders export",
+		"revenue breakdown by marketing channel",
+	}
+	files := []string{"orders.csv", "exports/orders.csv", "orders.tsv"}
+	channelAliases := []string{"channel", "source", "utm_source"}
+	revenueAliases := []string{"revenue", "amount", "price", "total"}
+
+	hegel.Test(t, func(ht *hegel.T) {
+		runs := hegel.Draw(ht, hegel.Integers(0, 50))
+		fails := hegel.Draw(ht, hegel.Integers(0, runs))
+		task := hegel.Draw(ht, hegel.SampledFrom(tasks))
+		file := hegel.Draw(ht, hegel.SampledFrom(files))
+		channel := hegel.Draw(ht, hegel.SampledFrom(channelAliases))
+		revenue := hegel.Draw(ht, hegel.SampledFrom(revenueAliases))
+
+		active := revenueRecipe("active", runs, fails)
+		stale := revenueRecipe("stale", runs, fails)
+		stale.MarkStale()
+		q := retrieve.Query{Task: task, Files: []string{file}, Columns: []string{channel, revenue}}
+
+		activeScore := retrieve.Rank([]*recipe.Recipe{active}, q, cfg)[0].Score
+		staleHit := retrieve.Rank([]*recipe.Recipe{stale}, q, cfg)[0]
+		if !near(staleHit.Score, activeScore*0.5) {
+			failProperty(ht, "PROP-retrieval-stale-penalty", map[string]any{
+				"runs":         runs,
+				"failures":     fails,
+				"task":         task,
+				"file":         file,
+				"channel":      channel,
+				"revenue":      revenue,
+				"active_score": activeScore,
+				"stale_score":  staleHit.Score,
+			}, "stale score %.6f, active %.6f; want exact half", staleHit.Score, activeScore)
+		}
+		if !hasReason(staleHit, "stale") {
+			failProperty(ht, "PROP-retrieval-stale-penalty", map[string]any{
+				"runs":     runs,
+				"failures": fails,
+				"task":     task,
+				"file":     file,
+				"channel":  channel,
+				"revenue":  revenue,
+				"reasons":  staleHit.Reasons,
+			}, "stale hit did not carry stale reason: %v", staleHit.Reasons)
+		}
+	}, hegelOpts(t, 50)...)
+}
+
+func propRetrievalSignalMonotonicity(t *testing.T) {
+	cfg := config.Default().Retrieval
+	channelAliases := []string{"channel", "source", "utm_source"}
+	revenueAliases := []string{"revenue", "amount", "price", "total"}
+	files := []string{"orders.csv", "exports/orders.csv"}
+	badColumns := []string{"sku", "customer", "created_at", "country"}
+
+	hegel.Test(t, func(ht *hegel.T) {
+		channel := hegel.Draw(ht, hegel.SampledFrom(channelAliases))
+		revenue := hegel.Draw(ht, hegel.SampledFrom(revenueAliases))
+		file := hegel.Draw(ht, hegel.SampledFrom(files))
+		badA := hegel.Draw(ht, hegel.SampledFrom(badColumns))
+		badB := hegel.Draw(ht, hegel.SampledFrom(badColumns))
+		r := revenueRecipe("revenue", 10, 0)
+
+		base := retrieve.Rank([]*recipe.Recipe{r}, retrieve.Query{Task: "compute revenue by channel"}, cfg)[0]
+		matched := retrieve.Rank([]*recipe.Recipe{r}, retrieve.Query{
+			Task:    "compute revenue by channel",
+			Files:   []string{file},
+			Columns: []string{channel, revenue},
+		}, cfg)[0]
+		if matched.Score < base.Score {
+			failProperty(ht, "PROP-retrieval-signal-monotonicity", map[string]any{
+				"channel":       channel,
+				"revenue":       revenue,
+				"file":          file,
+				"base_score":    base.Score,
+				"matched_score": matched.Score,
+			}, "matching structural signals lowered score: base %.6f matched %.6f", base.Score, matched.Score)
+		}
+		if matched.SignalMatch != 1.0 {
+			failProperty(ht, "PROP-retrieval-signal-monotonicity", map[string]any{
+				"channel":      channel,
+				"revenue":      revenue,
+				"file":         file,
+				"signal_match": matched.SignalMatch,
+			}, "matching file+columns signal = %.2f, want 1.0", matched.SignalMatch)
+		}
+
+		unsatisfied := retrieve.Rank([]*recipe.Recipe{r}, retrieve.Query{
+			Task:    "compute revenue by channel",
+			Columns: []string{badA, badB},
+		}, cfg)[0]
+		if unsatisfied.SignalMatch != 0 {
+			failProperty(ht, "PROP-retrieval-signal-monotonicity", map[string]any{
+				"bad_columns":   []string{badA, badB},
+				"signal_match":  unsatisfied.SignalMatch,
+				"matched_score": unsatisfied.Score,
+			}, "unsatisfied columns earned signal %.2f", unsatisfied.SignalMatch)
+		}
+		if !near(unsatisfied.Score, base.Score) {
+			failProperty(ht, "PROP-retrieval-signal-monotonicity", map[string]any{
+				"bad_columns":       []string{badA, badB},
+				"base_score":        base.Score,
+				"unsatisfied_score": unsatisfied.Score,
+			}, "unsatisfied columns changed lexical-only score: base %.6f unsatisfied %.6f", base.Score, unsatisfied.Score)
+		}
+	}, hegelOpts(t, 50)...)
+}
+
+func propRunnerTrustGate(t *testing.T) {
+	hegel.Test(t, func(ht *hegel.T) {
+		verifierPasses := hegel.Draw(ht, hegel.Booleans())
+		artifactDeclared := hegel.Draw(ht, hegel.Booleans())
+		artifactExists := hegel.Draw(ht, hegel.Booleans())
+
+		dir, err := os.MkdirTemp("", "chant-hegel-runner-")
+		if err != nil {
+			ht.Fatalf("temp dir: %v", err)
+		}
+		defer os.RemoveAll(dir)
+
+		verifier := "true"
+		if !verifierPasses {
+			verifier = "false"
+		}
+		var artifacts []string
+		if artifactDeclared {
+			artifacts = []string{"out.txt"}
+			if artifactExists {
+				if err := os.WriteFile(filepath.Join(dir, "out.txt"), []byte("ok\n"), 0o644); err != nil {
+					ht.Fatalf("write artifact: %v", err)
+				}
+			}
+		}
+		rc := &recipe.Recipe{
+			ID:           "runner-prop",
+			WhatToDo:     recipe.WhatToDo{Command: "true"},
+			Verification: recipe.Verification{Command: verifier, ExpectedArtifacts: artifacts},
+		}
+		rc.SetDir(dir)
+
+		res, trusted, err := runner.Verify(rc, nil, 5*time.Second)
+		if err != nil {
+			failProperty(ht, "PROP-runner-trust-gate", map[string]any{
+				"verifier_passes":   verifierPasses,
+				"artifact_declared": artifactDeclared,
+				"artifact_exists":   artifactExists,
+				"error":             err.Error(),
+			}, "Verify returned command-level error: %v", err)
+		}
+		want := verifierPasses && (!artifactDeclared || artifactExists)
+		if trusted != want {
+			failProperty(ht, "PROP-runner-trust-gate", map[string]any{
+				"verifier_passes":   verifierPasses,
+				"artifact_declared": artifactDeclared,
+				"artifact_exists":   artifactExists,
+				"trusted":           trusted,
+				"want":              want,
+				"exit_code":         res.ExitCode,
+				"stdout":            res.Stdout,
+				"stderr":            res.Stderr,
+			}, "trusted=%v, want %v (verifierPasses=%v artifactDeclared=%v artifactExists=%v res=%+v)",
+				trusted, want, verifierPasses, artifactDeclared, artifactExists, res)
+		}
+	}, hegelOpts(t, 50)...)
+}
+
+func propSpellHashStability(t *testing.T) {
+	placeholders := []string{"input", "file", "orders", "orders.csv", "input_file"}
+	hegel.Test(t, func(ht *hegel.T) {
+		aName := hegel.Draw(ht, hegel.SampledFrom(placeholders))
+		bName := hegel.Draw(ht, hegel.SampledFrom(placeholders))
+		swapGroups := hegel.Draw(ht, hegel.Booleans())
+		swapAliases := hegel.Draw(ht, hegel.Booleans())
+
+		colsA := [][]string{{"channel", "source"}, {"amount", "revenue"}}
+		colsB := [][]string{{"source", "channel"}, {"revenue", "amount"}}
+		if swapAliases {
+			colsB = [][]string{{"channel", "source"}, {"amount", "revenue"}}
+		}
+		if swapGroups {
+			colsB[0], colsB[1] = colsB[1], colsB[0]
+		}
+
+		a := &recipe.Recipe{
+			WhatToDo:    recipe.WhatToDo{Command: fmt.Sprintf("python3 run.py {{%s}}", aName)},
+			Portability: recipe.Portability{InputContract: recipe.InputContract{RequiredColumnsAny: colsA}},
+		}
+		b := &recipe.Recipe{
+			WhatToDo:    recipe.WhatToDo{Command: fmt.Sprintf("python3 \t run.py   {{ %s }}", bName)},
+			Portability: recipe.Portability{InputContract: recipe.InputContract{RequiredColumnsAny: colsB}},
+		}
+		if a.ComputeSpellHash() != b.ComputeSpellHash() {
+			failProperty(ht, "PROP-spell-hash-stability", map[string]any{
+				"placeholder_a": aName,
+				"placeholder_b": bName,
+				"swap_groups":   swapGroups,
+				"swap_aliases":  swapAliases,
+				"columns_a":     colsA,
+				"columns_b":     colsB,
+				"hash_a":        a.ComputeSpellHash(),
+				"hash_b":        b.ComputeSpellHash(),
+			}, "equivalent spell hashes differed: %s != %s", a.ComputeSpellHash(), b.ComputeSpellHash())
+		}
+	}, hegelOpts(t, 50)...)
+}
+
+func propCSVRecipeOracle(t *testing.T) {
+	root := repoRoot(t)
+	channelAliases := []string{"channel", "source", "utm_source"}
+	revenueAliases := []string{"revenue", "amount", "price", "total"}
+	rowGen := hegel.Composite(func(tc hegel.TestCase) csvPropRow {
+		return csvPropRow{
+			Channel: hegel.Draw(tc, hegel.SampledFrom([]string{"google", "facebook", "direct", "email", "", " google "})),
+			Revenue: hegel.Draw(tc, hegel.SampledFrom([]string{"0", "1", "1.25", "200", "bad", "", " -3.5 ", "2.5"})),
+		}
+	})
+
+	hegel.Test(t, func(ht *hegel.T) {
+		channelCol := hegel.Draw(ht, hegel.SampledFrom(channelAliases))
+		revenueCol := hegel.Draw(ht, hegel.SampledFrom(revenueAliases))
+		rows := hegel.Draw(ht, hegel.Lists(rowGen).MaxSize(12))
+		want := csvOracle(rows)
+
+		got, err := runCSVRecipe(root, channelCol, revenueCol, rows)
+		if err != nil {
+			failProperty(ht, "PROP-csv-recipe-oracle", map[string]any{
+				"channel_column": channelCol,
+				"revenue_column": revenueCol,
+				"rows":           rows,
+				"error":          err.Error(),
+			}, "run csv recipe: %v", err)
+		}
+		if !mapsNear(got, want) {
+			failProperty(ht, "PROP-csv-recipe-oracle", map[string]any{
+				"channel_column": channelCol,
+				"revenue_column": revenueCol,
+				"rows":           rows,
+				"got":            got,
+				"want":           want,
+			}, "csv totals mismatch:\n got=%v\nwant=%v\nrows=%+v", got, want, rows)
+		}
+
+		reversed := append([]csvPropRow(nil), rows...)
+		for i, j := 0, len(reversed)-1; i < j; i, j = i+1, j-1 {
+			reversed[i], reversed[j] = reversed[j], reversed[i]
+		}
+		gotReversed, err := runCSVRecipe(root, channelCol, revenueCol, reversed)
+		if err != nil {
+			failProperty(ht, "PROP-csv-recipe-oracle", map[string]any{
+				"channel_column": channelCol,
+				"revenue_column": revenueCol,
+				"rows":           reversed,
+				"error":          err.Error(),
+			}, "run reversed csv recipe: %v", err)
+		}
+		if !mapsNear(gotReversed, want) {
+			failProperty(ht, "PROP-csv-recipe-oracle", map[string]any{
+				"channel_column": channelCol,
+				"revenue_column": revenueCol,
+				"rows":           reversed,
+				"got":            gotReversed,
+				"want":           want,
+			}, "csv totals changed under row reversal:\n got=%v\nwant=%v\nrows=%+v", gotReversed, want, reversed)
+		}
+	}, hegelOpts(t, 25)...)
+}
+
+func revenueRecipe(id string, runs, fails int) *recipe.Recipe {
+	return &recipe.Recipe{
+		ID:          id,
+		Version:     1,
+		Description: "Compute ecommerce revenue by channel from CSV-like exports",
+		WhenToUse: recipe.WhenToUse{
+			TaskPatterns: []string{"compute revenue by channel from csv", "analyze ecommerce orders export", "revenue breakdown by marketing channel"},
+			Tags:         []string{"csv", "ecommerce", "revenue", "analytics"},
+			InputSignals: recipe.InputSignals{
+				Files:      []string{"*.csv"},
+				ColumnsAny: [][]string{{"channel", "source", "utm_source"}, {"revenue", "amount", "price", "total"}},
+			},
+		},
+		Metrics: recipe.Metrics{Runs: runs, Failures: fails},
+	}
+}
+
+func hasReason(m retrieve.Match, needle string) bool {
+	for _, reason := range m.Reasons {
+		if strings.Contains(reason, needle) {
+			return true
+		}
+	}
+	return false
+}
+
+func near(a, b float64) bool {
+	return math.Abs(a-b) < 1e-9
+}
+
+func failProperty(ht *hegel.T, propertyID string, payload map[string]any, format string, args ...any) {
+	_, _ = recordPropertyFailure(os.Getenv("CHANT_HEGEL_FAILURE_DIR"), propertyID, payload)
+	ht.Fatalf(format, args...)
+}
+
+type csvPropRow struct {
+	Channel string
+	Revenue string
+}
+
+func runCSVRecipe(root, channelCol, revenueCol string, rows []csvPropRow) (map[string]float64, error) {
+	dir, err := os.MkdirTemp("", "chant-hegel-csv-")
+	if err != nil {
+		return nil, err
+	}
+	defer os.RemoveAll(dir)
+
+	src := filepath.Join(root, "recipes", "csv-revenue-by-channel", "run.py")
+	b, err := os.ReadFile(src)
+	if err != nil {
+		return nil, err
+	}
+	runPath := filepath.Join(dir, "run.py")
+	if err := os.WriteFile(runPath, b, 0o755); err != nil {
+		return nil, err
+	}
+
+	csvPath := filepath.Join(dir, "orders.csv")
+	f, err := os.Create(csvPath)
+	if err != nil {
+		return nil, err
+	}
+	w := csv.NewWriter(f)
+	if err := w.Write([]string{channelCol, revenueCol, "note"}); err != nil {
+		f.Close()
+		return nil, err
+	}
+	for _, row := range rows {
+		if err := w.Write([]string{row.Channel, row.Revenue, "generated"}); err != nil {
+			f.Close()
+			return nil, err
+		}
+	}
+	w.Flush()
+	if err := w.Error(); err != nil {
+		f.Close()
+		return nil, err
+	}
+	if err := f.Close(); err != nil {
+		return nil, err
+	}
+
+	cmd := exec.Command("python3", runPath, csvPath)
+	out, err := cmd.CombinedOutput()
+	if err != nil {
+		return nil, fmt.Errorf("%v: %s", err, strings.TrimSpace(string(out)))
+	}
+	var got map[string]float64
+	outJSON, err := os.ReadFile(filepath.Join(dir, "revenue_by_channel.json"))
+	if err != nil {
+		return nil, err
+	}
+	if err := json.Unmarshal(outJSON, &got); err != nil {
+		return nil, err
+	}
+	return got, nil
+}
+
+func csvOracle(rows []csvPropRow) map[string]float64 {
+	totals := map[string]float64{}
+	for _, row := range rows {
+		ch := strings.TrimSpace(row.Channel)
+		if ch == "" {
+			continue
+		}
+		rev, err := strconv.ParseFloat(strings.TrimSpace(row.Revenue), 64)
+		if err != nil {
+			rev = 0
+		}
+		totals[ch] = math.Round((totals[ch]+rev)*100) / 100
+	}
+	return totals
+}
+
+func mapsNear(a, b map[string]float64) bool {
+	if len(a) != len(b) {
+		return false
+	}
+	for k, av := range a {
+		bv, ok := b[k]
+		if !ok || !near(av, bv) {
+			return false
+		}
+	}
+	return true
+}
+
+func repoRoot(t *testing.T) string {
+	t.Helper()
+	if root := os.Getenv("CHANT_REPO_ROOT"); root != "" {
+		return root
+	}
+	wd, err := os.Getwd()
+	if err != nil {
+		t.Fatalf("getwd: %v", err)
+	}
+	for dir := wd; ; dir = filepath.Dir(dir) {
+		if _, err := os.Stat(filepath.Join(dir, "go.mod")); err == nil {
+			if _, err := os.Stat(filepath.Join(dir, "recipes", "csv-revenue-by-channel", "run.py")); err == nil {
+				return dir
+			}
+		}
+		parent := filepath.Dir(dir)
+		if parent == dir {
+			t.Fatalf("could not find repo root from %s", wd)
+		}
+	}
+}