Proof Portal

Sign in
Project overview

Omarchy

ProbeLabs65 findings · 95 requirements

A proof layer — requirements, tests and verified fixes — for two of Omarchy's subsystems: the application menu (launcher scripts, QML model, JSONC config, search and selection) and the lock screen (lock scripts, QML, PAM authentication). Scope is deliberately limited to those components of omacom/omarchy; the rest of the distribution is not covered.

Inbox
ReportR-102GitHub issuePublicFixed

Menu JSONC: labels containing `, ]` or `, }` are silently corrupted by the trailing-comma stripper

Reported by buger · filed Sep 25, 2026 · open at source · 4 revisions

Open at source
Decided: Duplicate — decided by agents · verified 3 days ago.

At a glance

1 · What is claimed?
  • ConfirmedViolates SW-REQ-260922-E4J2: a label containing ', ]' or ', }' loses its comma: the parsed item no longer carries the authored label
  • ConfirmedReproducible: parseMenuJsonc('{"b":{"label":"x, ]y"}}') returns label 'x ]y'
  • ConfirmedAffects the menu component
  • LinkedMatches known issue KI-MENU-JSONC-COMMA-IN-STRING
2 · What does it affect?
AreaIn the audited areamenu· Decided by agents · verified
3 · Is it reproducible?
An engine-executed run exited 1 and showed the defect signal. See reproducer
4 · What remains unclear?
  • Open question for maintainers: Does any shipped or user menu.jsonc contain a label or action with ', ]' or ', }'? None ships one; the impact is silent corruption when it happens (an action like 'mv f{.bak,}' changes meaning).
  • Open question for maintainers: #13968, #13305, #6525 and #13681 touch the same lines of MenuModel.js; whichever lands first makes the others conflict.
5 · What happens next?
Decided by agents and verified by a second, independent agent — see the decision.

Original report

Revision1234 (current)
Menu JSONC: labels containing `, ]` or `, }` are silently corrupted by the trailing-comma stripperrevision 1 · captured 2026-09-28 21:23 UTC via poll

A menu label that contains a comma followed by whitespace and ] or } gets silently rewritten — the comma is eaten — because the trailing-comma "repair" fires inside string literals.

Reproduced on current master (d201fb95), using the repo's own parser, stock file fetched straight from this repo (narrated, 60s):

https://github.com/user-attachments/assets/e6f9f12f-8f19-449b-97c6-8ef5241f2ccb

Repro (run from the repo root, node ≥ 18):

// repro.js
const m = require("./shell/plugins/menu/MenuModel.js");

const menu = JSON.stringify({ b: { label: "x, ]y" } });  // label literally contains ", ]"

const rows = m.parseMenuJsonc(menu);
console.log("label:", JSON.stringify(rows[0].label));
// expected: "x, ]y"   actual: "x ]y" — the comma is silently gone

What happens. stripJsonc (MenuModel.js:2-5) removes trailing commas with

.replace(/,(\s*[}\]])/g, "$1")

The regex has no notion of string literals, so the sequence , ] inside a quoted label matches and gets "repaired" as if it were a trailing comma. The result is still valid JSON, so parsing succeeds and the corruption is invisible — the user just sees a label that isn't what they wrote.

Relationship to #6525. The open PR #6525 fixes the comment-stripping half of this function with a string-aware scanner, but keeps this comma regex untouched — verified: the corruption above still reproduces on its head. The same string-aware technique applies here; we have a minimal fix ready (a comma is dropped only when it occurs outside a string) and will raise it as a PR shortly. The two compose cleanly: whichever lands second is a one-function rebase.

Found while auditing the menu component with [Proof](https://reqproof.com) — formal verification with full MC/DC coverage of the menu's bash and QML code paths.

View raw text
A menu label that contains a comma followed by whitespace and `]` or `}` gets silently rewritten — the comma is eaten — because the trailing-comma "repair" fires *inside* string literals.

Reproduced on current master (`d201fb95`), using the repo's own parser, stock file fetched straight from this repo (narrated, 60s):

https://github.com/user-attachments/assets/e6f9f12f-8f19-449b-97c6-8ef5241f2ccb

**Repro** (run from the repo root, node ≥ 18):

```js
// repro.js
const m = require("./shell/plugins/menu/MenuModel.js");

const menu = JSON.stringify({ b: { label: "x, ]y" } });  // label literally contains ", ]"

const rows = m.parseMenuJsonc(menu);
console.log("label:", JSON.stringify(rows[0].label));
// expected: "x, ]y"   actual: "x ]y" — the comma is silently gone
```

**What happens.** `stripJsonc` (MenuModel.js:2-5) removes trailing commas with

```js
.replace(/,(\s*[}\]])/g, "$1")
```

The regex has no notion of string literals, so the sequence `, ]` *inside* a quoted label matches and gets "repaired" as if it were a trailing comma. The result is still valid JSON, so parsing succeeds and the corruption is invisible — the user just sees a label that isn't what they wrote.

**Relationship to #6525.** The open PR #6525 fixes the comment-stripping half of this function with a string-aware scanner, but keeps this comma regex untouched — verified: the corruption above still reproduces on its head. The same string-aware technique applies here; we have a minimal fix ready (a comma is dropped only when it occurs outside a string) and will raise it as a PR shortly. The two compose cleanly: whichever lands second is a one-function rebase.

*Found while auditing the menu component with [Proof](https://reqproof.com) — formal verification with full MC/DC coverage of the menu's bash and QML code paths.*
  • e6f9f12f-8f19-449b-97c6-8ef5241f2ccb

Validation

AI validator claude-code (claude-opus-5.5) · evaluated revision 4 at product commit 1e43373287af · sealed 2026-10-04T21:45:43Z

Validator's summary (commentary, not evidence)

Re-validation of omacom/omarchy#13250 (latest revision, edited 2026-10-02) on quattro-proof 1e433732 (upstream quattro 035ce29f product code plus the proof layer). The menu parser is unchanged since the previous validation (311d29c7..1e433732 merges upstream 035ce29f, whose only menu changes are two data rows in the stock omarchy-menu.jsonc (Install/Remove > Service > Microsoft), the image-picker helper bin/omarchy-menu-images and one display property on the bar's menu button; Menu.qml, MenuModel.js, ConfirmDialog.qml and omarchy-menu-select are byte-identical, and the rest is lock-screen and other non-menu upstream changes plus proof-layer records), and the result holds. A comma that sits before ']' or '}' inside a string is removed, because the trailing-comma regex in stripJsonc also fires inside string literals. SW-REQ-260922-E4J2 says trailing commas are stripped 'so the authored JSONC parses to its declared entries'. The reproducer (test/reports/, parser level, node over the real MenuModel.js) gets 'x ]y' and 'a }b' back for the labels 'x, ]y' and 'a, }b'; a real trailing comma is still dropped (control). Real entry path, checked separately in the running shell: a user extension entry labelled 'Keep, ]x' renders as 'Keep ]x' in the root menu on this baseline and as 'Keep, ]x' with #13968 merged. The baseline tracks the defect as KI-MENU-JSONC-COMMA-IN-STRING (open). The report's latest revision names #13968 as the fix and #13305 as a standalone fix, and says #6525 leaves it in place: all three statements reproduce (see comparative runs). The reproducer was re-run on 1e433732 with identical output; the live-shell runs are reused from 20d4e6ae (author-recorded): Menu.qml, MenuModel.js and omarchy-menu-select are unchanged since then apart from comment-only trace lines, and the two stock-menu rows added since (Install/Remove > Service > Microsoft) are outside what these runs exercise.

  • ConfirmedViolates a requirementThe parser strips full-line // comments and trailing commas… SW-REQ-260922-E4J2

    Violates SW-REQ-260922-E4J2: a label containing ', ]' or ', }' loses its comma: the parsed item no longer carries the authored label

    Engine: engine-executed run exited 1 and showed the defect signal

    What “confirmed” means here: the requirement exists and the engine reproduced the defect. That the reproducer exercises THIS requirement is the validator's argument (see rationale).

    Evidence: requirement SW-REQ-260922-E4J2 · file test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh

    Validator's rationale (commentary): SW-REQ-260922-E4J2: 'The parser strips full-line // comments and trailing commas before JSON parsing, so the authored JSONC parses to its declared entries.' A comma inside a string literal is not a trailing comma; removing it makes the item differ from its declaration. The reproducer asserts that the declared labels come back verbatim.

  • ConfirmedReproducible

    Reproducible: parseMenuJsonc('{"b":{"label":"x, ]y"}}') returns label 'x ]y'

    Engine: engine-executed run exited 1 and showed the defect signal

    Evidence: file test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh

  • ConfirmedAffects a componentmenu

    Affects the menu component

    Engine: confirmed violation of SW-REQ-260922-E4J2 owned by menu

    Evidence: requirement SW-REQ-260922-E4J2 · file test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh

  • LinkedDuplicate ofstripJsonc comma regex rewrites strings that carry a comma before } or ] (omacom/omarchy#13250) KI-MENU-JSONC-COMMA-IN-STRING

    Matches known issue KI-MENU-JSONC-COMMA-IN-STRING

    Engine: the known issue exists; whether the report duplicates it is settled by a human disposition; it affects the mapped requirement(s) SW-REQ-260922-E4J2

    Evidence: known_issue KI-MENU-JSONC-COMMA-IN-STRING · requirement SW-REQ-260922-E4J2

    Validator's rationale (commentary): The baseline KI records exactly this defect (comma before } or ] inside a string is rewritten) and links #13250.

Known issues examined for duplicates
Engine reference checks at 1e43373287af (9/9 ok)
  • okcommit1e43373287afbd6dca4674ad463d5b5db7812358
  • okbase commit1e43373287afbd6dca4674ad463d5b5db7812358
  • okbase ancestry1e43373287afbd6dca4674ad463d5b5db7812358
  • okproduct code untouchedthis report's reproducer branch
  • okbranchthis report's reproducer branch
  • okfiletest/reports/report-cmulr8l6h0i461gw40vqqv64c.sh
  • okrequirementSW-REQ-260922-E4J2
  • okcomponentmenu
  • okknown issueKI-MENU-JSONC-COMMA-IN-STRING

The engine's own check, at validation time, that the commits, the reproducer branch (touching only reproducer files), the reproducer files and every mapped requirement / component / known issue really exist.

10 earlier checks — superseded by the newest one above

Each new check of the report replaces the previous one; only the newest result above counts. Earlier results are kept for the record.

  • Reproduced— checked report revision 4 on Oct 4, 2026; earlier check, superseded
  • Reproduced— checked report revision 4 on Oct 3, 2026; earlier check, superseded
  • Reproduced— checked report revision 4 on Oct 3, 2026; earlier check, superseded
  • Reproduced— checked report revision 4 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 4 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 4 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 3 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 1 on Oct 1, 2026; earlier check, superseded
  • Refuted— checked report revision 1 on Oct 1, 2026; earlier check, superseded
  • Reproduced— checked report revision 1 on Sep 29, 2026; earlier check, superseded

Validator-authored hypothesis. Each claim's verification is engine-computed: confirmed only from an engine-executed reproducer run recorded in this record, refuted when recorded evidence contradicts it. Prose is commentary. The disposition of the report is a human decision.

Reproducer

engine-runexit 1 · expected exit 0 · defect exit 1 · 28 ms · 2026-10-04T21:45:43Z→ showed the defect
test/reports/report-cmulr8l6h0i461gw40vqqv64c.shon this report's reproducer branch @ 1e43373287
sh test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh

Setup failure: exit 2 means the reproducer could not set up (e.g. the product did not build) — such a run decides nothing.

Defect signal: output contains DEFECT:

Matched lines (engine, over the full output)
DEFECT: label containing ', ]' survives -- input "{\"b\":{\"label\":\"x, ]y\"}}" -> rows ["b=\"x ]y\""] (expected ["b=\"x, ]y\""])
DEFECT: label containing ', }' survives -- input "{\"b\":{\"label\":\"a, }b\"}}" -> rows ["b=\"a }b\""] (expected ["b=\"a, }b\""])
Observed output · 428 bytes
DEFECT: label containing ', ]' survives -- input "{\"b\":{\"label\":\"x, ]y\"}}" -> rows ["b=\"x ]y\""] (expected ["b=\"x, ]y\""])
DEFECT: label containing ', }' survives -- input "{\"b\":{\"label\":\"a, }b\"}}" -> rows ["b=\"a }b\""] (expected ["b=\"a, }b\""])
ok: control: trailing commas outside strings are still dropped -- input "{\"a\": {\"label\": \"A\",},}" -> rows ["a=\"A\""]
RESULT: 2 case(s) violate the requirement

Needs: linux · node >= 18 on PATH (the script exits 2 with SETUP: otherwise); nothing to build: MenuModel.js is plain JavaScript loaded straight from the worktree · ran on linux/amd64

Author's comparative runs — commentary, not engine evidence
  • author-recordedon this baseline with upstream PR omacom/omarchy#13968 head b2dae8db merged · exit 0
    sh test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh
    RESULT: all cases parse to the declared entries
  • author-recordedon upstream PR omacom/omarchy#13305 head bcd1ee39 (its MenuModel.js over this baseline) · exit 0
    sh test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh
    RESULT: all cases parse to the declared entries
  • author-recordedon upstream PR omacom/omarchy#6525 head 913e112d (its MenuModel.js over this baseline) · exit 1
    sh test/reports/report-cmulr8l6h0i461gw40vqqv64c.sh
    DEFECT: label containing ', ]' survives ... RESULT: 2 case(s) violate the requirement
  • author-recordedon live shell: Quickshell 0.3.1 on a headless sway compositor, the tree's own shell and stock menu, the user extension file ~/.config/omarchy/extensions/omarchy-menu.jsonc read by the shell's FileView; rows read back through a read-only IPC probe injected into a private copy; this baseline [run on 20d4e6ae, same menu code] · exit 1
    user extension: {"probe-keep": {"label": "Keep, ]x", "action": "echo f{.bak,}"}, ...}
    root menu row id=probe-keep label="Keep ]x" (comma lost)
  • author-recordedon live shell: Quickshell 0.3.1 on a headless sway compositor, the tree's own shell and stock menu, the user extension file ~/.config/omarchy/extensions/omarchy-menu.jsonc read by the shell's FileView; rows read back through a read-only IPC probe injected into a private copy; this baseline with upstream PR omacom/omarchy#13968 head b2dae8db merged [run on 20d4e6ae, same menu code] · exit 0
    same user extension file
    root menu row id=probe-keep label="Keep, ]x" (verbatim)

Linked

Decision

Decisions are recorded by our staff — or, where this project allows it, by agents: checked by a second, independent agent, or by a single agent where the project's policy says so. Any decision reached so far is shown below.