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.
Coding agents can't sign commits unattended
Reported by chriopter · filed Sep 10, 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
Omarchy treats coding agents as first-class citizens, but an agent working while nobody is at the keyboard can't sign its commits: the signing key needs an unlock, and 1Password is locked. So those commits either fail or go unsigned.
The workaround that doesn't need anything from Omarchy is an unencrypted key on disk — which works forever for whoever leaks it.
A TPM key fixes that shape of problem: generated inside the chip, so it never exists as bytes and can't be copied off the machine, and it signs with no prompt. The pieces are all in extra (ssh-tpm-agent), and the gating is cheap — a menu row behind omarchy-hw-tpm and a unit behind ConditionPathExists cost nothing on a machine without a TPM.
Before writing more of it, two questions for maintainers:
- Is this Omarchy's problem to solve? I searched: no issue mentions commit signing,
gpgsign, or signing with an agent. That could mean the need is real but unarticulated, or that people who run agents simply don't sign. I'd rather ask than assume.
- How much access should reaching the TPM cost the user?
/dev/tpmrm0isroot:tss, and thetssgroup is full TPM command access, not permission to sign — I probed the chip to check, and an undefined command code passes straight through the kernel's resource manager to be rejected by the TPM itself. WithownerAuthunset (the default) code running as the user can take ownership or drive the dictionary-attack counter into a lockout only firmware clears. Stock Omarchy binds nothing else to the TPM, so today the blast radius is the signing key — but that holds only until someone adopts TPM-backed LUKS.
Three shapes, in the order I'd rank them:
- A system service under its own account in tss, handing users only a 0600 socket. The user's authority becomes "ask this one key for a signature" instead of "arbitrary TPM commands forever". ssh-tpm-agent already ships system units for this. Costs: keys move out of $HOME, removal needs privilege.
- The `tss` group, explained and confirmed before granting, undone on removal the way omarchy-remove-security-sudoless-docker undoes its own. Simplest, opt-in, per-user — but the grant outlives what it was for.
- A `uaccess` udev rule. I don't recommend it: it buys nothing against code running as you in your own session, breaks SSH and headless use, and would widen TPM access on every machine rather than staying opt-in.
I have a working branch of shape 2 — wizard, agent unit, tests, and a real signature verified against the chip — and would rework it to shape 1 if that's preferred. Happy to open it as a PR, or to drop the idea if the answer to (1) is no.
View raw text
Omarchy treats coding agents as first-class citizens, but an agent working while nobody is at the keyboard can't sign its commits: the signing key needs an unlock, and 1Password is locked. So those commits either fail or go unsigned. The workaround that doesn't need anything from Omarchy is an unencrypted key on disk — which works forever for whoever leaks it. A TPM key fixes that shape of problem: generated inside the chip, so it never exists as bytes and can't be copied off the machine, and it signs with no prompt. The pieces are all in `extra` (`ssh-tpm-agent`), and the gating is cheap — a menu row behind `omarchy-hw-tpm` and a unit behind `ConditionPathExists` cost nothing on a machine without a TPM. **Before writing more of it, two questions for maintainers:** 1. **Is this Omarchy's problem to solve?** I searched: no issue mentions commit signing, `gpgsign`, or signing with an agent. That could mean the need is real but unarticulated, or that people who run agents simply don't sign. I'd rather ask than assume. 2. **How much access should reaching the TPM cost the user?** `/dev/tpmrm0` is `root:tss`, and the `tss` group is full TPM command access, not permission to sign — I probed the chip to check, and an undefined command code passes straight through the kernel's resource manager to be rejected by the TPM itself. With `ownerAuth` unset (the default) code running as the user can take ownership or drive the dictionary-attack counter into a lockout only firmware clears. Stock Omarchy binds nothing else to the TPM, so today the blast radius is the signing key — but that holds only until someone adopts TPM-backed LUKS. Three shapes, in the order I'd rank them: - **A system service** under its own account in `tss`, handing users only a `0600` socket. The user's authority becomes "ask this one key for a signature" instead of "arbitrary TPM commands forever". `ssh-tpm-agent` already ships system units for this. Costs: keys move out of `$HOME`, removal needs privilege. - **The `tss` group**, explained and confirmed before granting, undone on removal the way `omarchy-remove-security-sudoless-docker` undoes its own. Simplest, opt-in, per-user — but the grant outlives what it was for. - **A `uaccess` udev rule.** I don't recommend it: it buys nothing against code running as you in your own session, breaks SSH and headless use, and would widen TPM access on every machine rather than staying opt-in. I have a working branch of shape 2 — wizard, agent unit, tests, and a real signature verified against the chip — and would rework it to shape 1 if that's preferred. Happy to open it as a PR, or to drop the idea if the answer to (1) is no.
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 13:32 UTC