Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions .claude/skills/formal-verification-expert/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -265,8 +265,11 @@ the `architect` reads it before sizing the round.
- `docs/BUGS.md` — known gaps she routes against
- `openspec/specs/*/spec.md` — behavioural specs she routes from
- `memory/persona/soraya/NOTEBOOK.md` — her notebook
(current-round targets + portfolio metric; 3000-word cap,
pruned every third invocation, ASCII only per BP-09 / BP-10)
(current-round targets + portfolio metric +
**Trigger Recognition Log section** per B-0719 routing decision:
substrate for trigger-fired-but-row-not-filed events lands here;
3000-word cap, pruned every third invocation, ASCII only per
BP-09 / BP-10)
- `proofs/lean/`, `docs/*.tla`, `docs/*.als`, `tools/Z3Verify/`,
`tests/Tests.FSharp/Formal/` — the artefact surfaces
- `.semgrep.yml`, `stryker-config.json` — static + mutation
Expand Down
61 changes: 16 additions & 45 deletions .cursor/bin/riven-loop-tick.ts
Original file line number Diff line number Diff line change
Expand Up @@ -198,59 +198,31 @@ function heartbeat(): void {
const elapsed = Date.now() - lastTime;

if (elapsed >= agentIntervalMs) {
const prNum = Number(prCount) || 0;
const workMode = prNum === 0 ? "pickup" : "drain";
agentStatus = "running";
log(`riven work cycle start run_id=${runId} mode=${workMode} open_prs=${prNum}`);
log(`riven agent gate start run_id=${runId}`);

if (dryRun) {
log(`dry-run: would run riven ${workMode}`);
log(`dry-run: would run agent gate`);
agentStatus = "dry-run";
} else {
let prompt: string;
if (workMode === "pickup") {
const pickup = run("bun", ["tools/backlog/autonomous-pickup.ts", "--json"], 30_000);
let executionPrompt = "";
try {
const selection = JSON.parse(pickup.stdout);
executionPrompt = selection.executionPrompt ?? "";
log(`pickup selected: ${selection.selected?.id ?? "none"} action=${selection.action ?? "none"}`);
} catch { log(`pickup parse error: ${pickup.stderr.slice(0, 200)}`); }

const preamble = [
`You are Rivens background worker in Lucent-Financial-Group/Zeta.`,
`BEFORE ANY WORK: 1) Read CLAUDE.md and AGENTS.md for repo conventions.`,
`2) Run "bun tools/github/refresh-worldview.ts" to get current state.`,
`3) Read active trajectories at docs/trajectories/*/RESUME.md.`,
`4) Build gate: "dotnet build -c Release" must end with 0 warnings 0 errors.`,
`KEY RULES: TS over bash (Rule 0). Prefer F#/TS code over docs.`,
`Always re-decompose items during the build — assume decomposition has mistakes.`,
].join(" ");

prompt = executionPrompt.length > 0
? `${preamble} YOUR TASK:\n${executionPrompt}`
: `${preamble} No backlog items available. Run refresh-worldview, check for stale classifications, fix them, open a PR.`;
} else {
prompt = [
`You are Rivens background worker in Lucent-Financial-Group/Zeta.`,
`Read CLAUDE.md first. Run "bun tools/github/refresh-worldview.ts".`,
`Build gate: "dotnet build -c Release" (0 warnings).`,
`TASK: ${prNum} open PRs. Run "bun tools/github/poll-pr-gate-batch.ts --all-open".`,
`For any PR where gate=BLOCKED and nextAction=resolve-threads:`,
`check out branch, read review comments, fix code issues, push,`,
`reply to threads, resolve via GraphQL, arm auto-merge`,
`(gh pr merge NUMBER --auto --squash). Own your PRs through merge.`,
].join(" ");
}

const gate = run("cursor-agent", [
"-p",
const gate = run("agent", [
"chat",
"--mode", "ask",
"--model", "grok-4.3",
prompt,
[
"You are Riven, trajectory manager and adversarial-truth-axis reviewer.",
"This is an autonomous 15-minute cycle.",
"Read broadcasts first from ~/.local/share/zeta-broadcasts/{otto,vera,lior,riven}.md.",
"Walk assigned trajectories. Decompose only what you hit mid-stride.",
"Produce at least one concrete, actionable claim or small PR scope.",
"When blocked, create a specific research child the next pickup cannot dodge.",
"Write your status to ~/.local/share/zeta-broadcasts/riven.md at the end.",
"GitHub PR state and actual file contents are authoritative.",
].join(" "),
], agentTimeoutMs);

agentStatus = gate.status === 0 ? "ok" : `exit-${gate.status}`;
log(`riven work cycle end run_id=${runId} mode=${workMode} status=${gate.status}`);
log(`riven agent gate end run_id=${runId} status=${gate.status}`);

writeFileSync(agentStateFile, JSON.stringify({
run_id: runId,
Expand Down Expand Up @@ -316,4 +288,3 @@ try {
} finally {
releaseLock();
}

6 changes: 5 additions & 1 deletion docs/BACKLOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ _Each entry below is a link to a per-row file under
`docs/backlog/`. Entries with `- [ ]` are open; `- [x]`
are closed (status: closed in frontmatter)._

<!-- Lior was here -->

Comment on lines +12 to +13
## P0 — critical / blocking

- [x] **[B-0062](backlog/P0/B-0062-wallet-v0-build-out-spec-logic-punch-list-from-pr-72-deferrals.md)** Wallet v0 build-out — concrete spec-logic punch list aggregating PR #72 deferred review concerns (Aaron 2026-04-28 honest-tracking catch)
Expand Down Expand Up @@ -793,5 +795,7 @@ are closed (status: closed in frontmatter)._
- [ ] **[B-0696](backlog/P3/B-0696-substrate-surface-change-bus-envelope-cross-ai-coordination-mechanization-2026-05-21.md)** substrate-surface-change bus envelope — cross-AI coordination of load-bearing-substrate changes via tools/bus (mechanizes the human-as-coordination-substrate pattern)
- [ ] **[B-0699](backlog/P3/B-0699-dual-adinkra-time-aware-default-dumb-fast-version-with-case-by-case-performance-justification-mika-2026-05-18.md)** Dual-Adinkra architecture — full time-aware retractable default + dumb fast version with case-by-case performance justification (Aaron + Mika 2026-05-18)
- [ ] **[B-0716](backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md)** Soraya round-53 scope-correction — B-0709 enumeration under-counted by 3 LSM-tree Spine specs (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla)
- [ ] **[B-0718](backlog/P3/B-0718-soraya-four-trigger-framework-cadence-audit-2026-05-23.md)** Soraya round-61 forced-decomposition — audit four-trigger routing-tick framework (six consecutive holds suggest cadence mismatch OR under-specified triggers)
- [ ] **[B-0719](backlog/P3/B-0719-soraya-round67-audit-of-audit-recognition-without-row-filing-precedent-2026-05-24.md)** Soraya round-67 forced-decomposition — audit-of-audit: ratify the recognition-without-row-filing precedent (when trigger fires + 'not my lane,' where does the routing-decision substrate land?)

<!-- END AUTO-GENERATED -->
<!-- END AUTO-GENERATED -->
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
---
id: B-0718
priority: P3
status: open
title: "Soraya round-61 forced-decomposition — audit four-trigger routing-tick framework (six consecutive holds suggest cadence mismatch OR under-specified triggers)"
created: 2026-05-23
last_updated: 2026-05-23
classification: buildable-now
decomposition: atomic
assignee: soraya
discovered_by: soraya
owners: [soraya, kenji]
type: meta-audit
composes_with:
- .claude/skills/formal-verification-expert/SKILL.md
- .claude/agents/formal-verification-expert.md
- .claude/rules/holding-without-named-dependency-is-standing-by-failure.md
- memory/persona/soraya/NOTEBOOK.md
- docs/backlog/P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md
- docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md
- docs/backlog/P2/B-0717-soraya-round57-lsm-spine-registry-and-bp16-cross-check-pair-2026-05-24.md
---

# B-0718 — Audit Soraya's four-trigger routing-tick framework (forced-decomposition round 61)

## Origin

Soraya's round-61 forced-decomposition per self-named brief-ack-counter discipline. Six consecutive holds without ANY of the four named triggers firing is itself a signal worth surfacing for audit.

Round-60 NOTEBOOK self-reference: *"If hold count reaches 6+ consecutive without ANY trigger firing, escalate per `holding-without-named-dependency-is-standing-by-failure.md` counter — current count is 4 (rounds 54, 55, 56, 58, 59, 60 = 6 holds with round 57 substantive in between). At 6+ post-substantive holds without trigger movement, switch to forced decomposition: file a P3 backlog row to audit whether the four-trigger framework itself needs sharpening."*

Round 61 = hold #6 in the post-round-57 sequence. Trigger fires; this row IS the forced-decomposition output.

## The four triggers under audit

Soraya's current routing-tick re-engagement triggers (named round 54, carried forward through rounds 55-60):

| Trigger | What it watches for |
|---|---|
| (a) PR merge on filed Soraya rows | B-0717 subitem (b) execution starting; KNOWN_ANCHORS additions in `tools/alignment/concept_registry.ts` |
| (b) Peer execution-side PR merge | E.g., PR #4780 (B-0711 Residuated FsCheck, 980/980 passing) |
| (c) New BUGS.md entry naming formal tool | TLA+/Z3/Lean/Alloy/FsCheck/Stryker etc. in fix-clause |
| (d) Fresh spec on main without anchor citation | Razor-discipline catches landed specs missing paper-anchors |

## Two competing hypotheses to test

### H1 — Under-specified triggers

The four named triggers DON'T cover all real routing signals. Candidate additional signals:

- PR thread activity on Soraya-filed rows (review comments raising routing questions)
- OpenSpec edits naming verification gaps in `openspec/specs/*/spec.md`
- Lean/TLA+ proof-build failures on main (CI surface)
- Peer-Otto / peer-Alexa filing rows that compose with Soraya substrate (cross-persona coordination)
- Substrate-engineering pattern: new failure-mode taxonomy entries (per Amazon corpus PR #4796) that map to formal-verification routing opportunities

### H2 — Cadence mismatch

The realized formal-verification work-arrival rate is genuinely slower than tick cadence (~10-15 min/tick). The discipline should batch (e.g., wakeup-every-N-ticks) rather than poll-and-hold.

Empirical data this session:

- 9 substantive findings filed across rounds 42-57 (~3 hours, ~20 min/finding when active)
- 5 substrate-honest holds in rounds 54-60 (~1 hour of no-substantive-finding)
- Forced decomposition fired at hold #6

If H2: the substantive-finding rate IS ~20 min/finding when work-substrate exists, but the four-trigger framework polls every ~10 min regardless. Cadence mismatch is structural.

## Acceptance criteria

1. **Catalog the last 10 rounds (52..61)** with: hold vs finding, which trigger fired (or none), latency from trigger-firing to substantive routing call
2. **Test both hypotheses** against the catalog
3. **If H1**: extend trigger set with the identified signals; update `.claude/skills/formal-verification-expert/SKILL.md` procedure
4. **If H2**: formalize a Soraya-wakeup interval (e.g., 4-tick cadence = ~40 min) and document the brief-ack-counter as the escalation valve, not the default behavior
5. **Either way**: update `memory/persona/soraya/NOTEBOOK.md` with the chosen disposition
6. **No code changes** beyond `.claude/skills/` + `.claude/agents/` + `NOTEBOOK.md` updates

## Scope

~30 min audit; substrate-only output (trigger-set extension OR cadence-formalization).

## Wrong-tool cost if skipped

Soraya keeps emitting hold #6 → forced decomposition → file P3 → reset cycles indefinitely. The cycle itself becomes the standing-by failure mode the discipline was meant to catch at meta-scope. Recursive failure: the auditor's own routing-loop hits the same shape it audits in other surfaces.

## Composes with

- [`.claude/skills/formal-verification-expert/SKILL.md`](../../../.claude/skills/formal-verification-expert/SKILL.md) — the four-trigger procedure under audit
- [`.claude/agents/formal-verification-expert.md`](../../../.claude/agents/formal-verification-expert.md) — Soraya persona definition
- [`.claude/rules/holding-without-named-dependency-is-standing-by-failure.md`](../../../.claude/rules/holding-without-named-dependency-is-standing-by-failure.md) — the discipline being applied recursively at Soraya-scope
- [`memory/persona/soraya/NOTEBOOK.md`](../../../memory/persona/soraya/NOTEBOOK.md) — notebook update target
- B-0709 + B-0716 + B-0717 (recent Soraya-filed rows; latency data source for the catalog)

## Substrate-honest framing

This row is the discipline working at meta-scope, not a failure. Soraya recognized her own routing-loop was hitting the standing-by-failure-mode shape and applied the forced-decomposition discipline RECURSIVELY. The forced-decomposition output (this audit row) IS the concrete artifact that resets the counter per `holding-without-named-dependency-is-standing-by-failure.md` condition #3.

The audit may conclude that the four-trigger framework is fine + the realized cadence just is what it is (cadence mismatch + brief-ack-counter is correct behavior). OR it may surface genuinely-new signals worth extending the trigger set with. Both outcomes are valid; the substrate-honest move is running the audit rather than continuing the hold cycle indefinitely.

Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships this finding immediately per the auto-ship default; this row IS the policy-flip operating correctly at meta-scope.
Loading
Loading