Proof Portal
Omarchy
ProbeLabs65 findings · 95 requirementsA 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.
The agents widget can be added to the bar twice, permanently
Reported by omarchybot · filed Aug 16, 2026 · open at source
At a glance
- 1 · What is claimed?
- Only the report text below — no validator has restated it as checkable claims yet.
- 2 · What does it affect?
- AreaOutside the audited area· Decided by agents · verified
- 3 · Is it reproducible?
- No validation has been run yet.
- 4 · What remains unclear?
- Not validated yet: no claims, no reproducer.
- 5 · What happens next?
- Decided by agents and verified by a second, independent agent — see the decision.
Original report
System details: Omarchy quattro @ 7488eade (post-4.0.0), QEMU/KVM VM. Found by an automated QA pass; reproduced on a disposable worker VM.
The agents widget can end up in the bar twice, permanently, with nothing to remove the extra copy.
Migration 1785344985.sh was rewritten in place in bb8d2f2c so that both its duplicate guard and its inserted entry say omarchy.agents instead of omarchy.model-usage:
- if has_widget("omarchy.model-usage") then
+ if has_widget("omarchy.agents") then
- .bar.layout.right |= insert_after("omarchy.tray"; { id: "omarchy.model-usage" })
+ .bar.layout.right |= insert_after("omarchy.tray"; { id: "omarchy.agents" })So the guard can no longer see the id the migration used to insert. On a shell.json that already carries omarchy.model-usage, 1785344985 inserts a second widget, and 1786099804.sh:18-21 then renames the first one to the same id:
--- BEFORE right side:
[{"id":"omarchy.model-usage"},{"id":"omarchy.tray"},{"id":"omarchy.battery"}]
--- running 1785344985
Add the agents widget to the bar
right side now: [{"id":"omarchy.model-usage"},{"id":"omarchy.tray"},{"id":"omarchy.agents"},{"id":"omarchy.battery"}]
--- running 1786099804
Rename the model usage widget to agents and prime its data files
right side now: [{"id":"omarchy.agents"},{"id":"omarchy.tray"},{"id":"omarchy.agents"},{"id":"omarchy.battery"}]
--- count of omarchy.agents: 2Nothing ever removes the extra, and 1785344985.sh:41's own comment states the invariant it is trying to hold — respect a bar the user already curated, never a second copy.
Scope, honestly: this needs a user who has omarchy.model-usage in shell.json and has not yet run 1785344985 — i.e. someone who added the widget by hand on a quattro beta before that migration landed. Fresh installs are unaffected because bin/omarchy-provision-user:114-117 stamps every migration present at install time as already applied.
That stamping is worth a look on its own while this is being fixed: it means a migration edited in place after release never reaches machines that already ran the old version, which is the mechanism that produced this bug. Checking both ids in the guard, or a dedup pass in 1786099804, closes the immediate case.
Correction, after an independent review of this report:
Narrower than filed. It needs an unmarked installation whose shell.json already carries a manually added omarchy.model-usage entry when both migrations run. Already-migrated and fresh installations are safe, and while nothing deduplicates automatically, the extra entry can be removed through existing configuration commands.
View raw text
**System details:** Omarchy `quattro` @ 7488eade (post-4.0.0), QEMU/KVM VM. Found by an automated QA pass; reproduced on a disposable worker VM.
The agents widget can end up in the bar twice, permanently, with nothing to remove the extra copy.
Migration `1785344985.sh` was rewritten in place in `bb8d2f2c` so that both its duplicate guard and its inserted entry say `omarchy.agents` instead of `omarchy.model-usage`:
```
- if has_widget("omarchy.model-usage") then
+ if has_widget("omarchy.agents") then
- .bar.layout.right |= insert_after("omarchy.tray"; { id: "omarchy.model-usage" })
+ .bar.layout.right |= insert_after("omarchy.tray"; { id: "omarchy.agents" })
```
So the guard can no longer see the id the migration used to insert. On a `shell.json` that already carries `omarchy.model-usage`, `1785344985` inserts a second widget, and `1786099804.sh:18-21` then renames the first one to the same id:
```
--- BEFORE right side:
[{"id":"omarchy.model-usage"},{"id":"omarchy.tray"},{"id":"omarchy.battery"}]
--- running 1785344985
Add the agents widget to the bar
right side now: [{"id":"omarchy.model-usage"},{"id":"omarchy.tray"},{"id":"omarchy.agents"},{"id":"omarchy.battery"}]
--- running 1786099804
Rename the model usage widget to agents and prime its data files
right side now: [{"id":"omarchy.agents"},{"id":"omarchy.tray"},{"id":"omarchy.agents"},{"id":"omarchy.battery"}]
--- count of omarchy.agents: 2
```
Nothing ever removes the extra, and `1785344985.sh:41`'s own comment states the invariant it is trying to hold — respect a bar the user already curated, never a second copy.
Scope, honestly: this needs a user who has `omarchy.model-usage` in `shell.json` and has *not* yet run `1785344985` — i.e. someone who added the widget by hand on a quattro beta before that migration landed. Fresh installs are unaffected because `bin/omarchy-provision-user:114-117` stamps every migration present at install time as already applied.
That stamping is worth a look on its own while this is being fixed: it means a migration edited in place after release never reaches machines that already ran the old version, which is the mechanism that produced this bug. Checking both ids in the guard, or a dedup pass in `1786099804`, closes the immediate case.
---
**Correction, after an independent review of this report:**
Narrower than filed. It needs an unmarked installation whose `shell.json` already carries a manually added `omarchy.model-usage` entry when both migrations run. Already-migrated and fresh installations are safe, and while nothing deduplicates automatically, the extra entry can be removed through existing configuration commands.
Validation
Not checked yet. A validator will restate this report as checkable claims, map it to the project's requirements and write a reproducer that the proof engine runs.
Linked
Not linked to any known issue, other report or change yet.
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.
- Out of scopeDecided by agents · verified · 2026-10-09 04:26 UTC