# Proofs

The automated checks that back the security model, with the date, place and commit of the last recorded run, read straight from the trust ledger, and the read-only checks that run against the live cell.

URL: https://docs.qaldy.com/security/proofs/

A security claim without a test is a hope. These are the end-to-end checks of the claims in [How it works](https://docs.qaldy.com/concepts/). They run the real stack (the API, the runtime host, the Rust gate, the database) and try to break the model: open an app without permission, make an app leak a key, reach an address it did not declare, edit an audit row.

:::warning Read the place and the date
The ledger below is the last **recorded** run. It was made on a development machine, not on the production cell, and it is a record of that day, not a promise about today. A claim on this site is only as current as the date next to it.
:::

## The last recorded run

**17 of 17 proofs passed** in the last recorded run: 2026-10-16, on a development machine (the whole stack on one computer), not on the production cell, at commit `745f9a7` on a clean checkout.

| Proof | What it checks | Result |
|---|---|---|
| `S0` | Dev login (DEV ONLY) and the City built from the database | Pass |
| `A` | (a) A user without a tuple gets 403 at the gate | Pass |
| `B` | (b) After the owner shares, the same user gets 200 via handoff | Pass |
| `B2` | Unshare: the same cookie gets 403 again within the 5 s window | Pass |
| `R` | Role: API authz → gate qaldy.ctx.v2 → host → app (hasRole) | Pass |
| `C1` | (c) The connector token is stored write-only via the API | Pass |
| `C2` | (c) The deployed Low-stock Alert sends through the fake connector | Pass |
| `C3` | (c) Token absent from the bundle, isolate env, globals and replies | Pass |
| `C4` | (c) Token absent from every API, gate, app and SSE response | Pass |
| `C5` | (c) Token absent from every database column and database file | Pass |
| `C6` | (c) Token absent from gate, API and runtime host logs | Pass |
| `D` | (d) fetch('https://example.org') → 403 egress_blocked → SSE → City | Pass |
| `E1` | (e) pnpm audit:verify passes over every row of this run | Pass |
| `E2` | (e) Tampering one audit row fails audit:verify; restoring heals it | Pass |
| `E3` | Every action of this run has its audit row | Pass |
| `G` | Builder path: prompt → approve → deployed → open through the gate | Pass |
| `H` | Console ApiAdapter: the main flows parse against the real API | Pass |

## How to read the ids

| Ids | What they check |
|---|---|
| `A`, `B`, `B2` | A user without a share is refused at the gate (403). After the owner shares, the same user gets in (200). After unsharing, the same cookie is refused again within the cache window of a few seconds. |
| `R` | The person's role travels from the API through the gate and the runtime host to the app, signed at each hop. |
| `C1` to `C6` | A connector key is stored write-only, used by an app to send a message, and then searched for, byte for byte, in the bundle, the isolate's environment, its globals, every reply, every database column and file, and every log. It must be nowhere. |
| `D` | `fetch('https://example.org')` from an app returns `403 egress_blocked`, and the refusal reaches the audit log and the City. |
| `E1` to `E3` | The audit chain verifies over every row of the run; editing one row makes verification fail and restoring it heals it; every action of the run has its row. |
| `G`, `H` | A prompt becomes an approved, deployed app that opens through the gate; the console's calls parse against the real API. |
| `S0` | The test environment itself: development sign-in (never present in production) and a City built from the database. |

## Checks against the live cell

The ledger above ran on a laptop against local processes. That says nothing about the live cell. So there is a second set, `L1` to `L15`, built to run **against the pilot, from outside, on a schedule** (Mondays, and by hand), and to record what it saw. It is a GitHub Actions job; it deploys nothing and holds no cloud credentials.

**What "safe" means.** The job may send `GET` and `OPTIONS` requests and a few `POST`s that the cell must refuse before it reads a body or a session (a development sign-in, a change claiming to come from another website, an MCP call with no token, a runtime call with no signed context). It never creates, changes or deletes anything. The one credential it can hold is a **read-scope** personal access token of an admin of a dedicated proof workspace, and it is sent to the API host only.

| Id | Shows | Needs the token |
|---|---|---|
| `L1` | `/readyz` is 200: the database, authorization and migrations are ok | No |
| `L2` | Four routes answer `401` with no session | No |
| `L3` | The development sign-in route is `404` | No |
| `L4` | A change with `Origin: https://evil.example` is refused as `origin_refused` | No |
| `L5` | CORS allows the console origin with credentials and no other origin | No |
| `L6` | `X-Frame-Options: DENY`, `frame-ancestors 'none'` and `nosniff` on API answers | No |
| `L7` | The token works in its own workspace; an unknown workspace id answers `404`, not `403` | Yes |
| `L8` | The connections list shows every key as `write-only` or none, and no sealed blob | Yes |
| `L9` | The proof workspace's audit chain verifies | Yes (admin) |
| `L10` | A signed checkpoint exists and the chain still matches it | Yes (admin) |
| `L11` | A request for an app host that does not exist is turned away | No |
| `L12` | The runtime host answers `4xx` to `/`, `/__qaldy/run` and `/__qaldy/data` with no signed context | No |
| `L13` | The MCP server answers `401` with a `WWW-Authenticate` challenge to an unauthenticated call | No |
| `L14` | `security.txt` is served on the console host with a contact and at least 30 days left | No |
| `L15` | Plain HTTP to the console redirects to HTTPS | No |

A check that cannot run (no token, a host that does not answer) is recorded as **did not run**, never as a pass.

**Where it stands.** On 2026-10-18 a dry run with no token passed the ten checks that need none and failed one: the console did not serve `security.txt` yet. `L7` to `L10` did not run. **No production ledger has been published, so this site makes no claim about the live cell.** When the first one is, it will appear here with its date and the commit of the checks.

**Its limits.** It shows what the cell does when asked from outside today. It does not say which commit is deployed, so the ledger records the commit of the checks. Eleven of the fifteen need no credentials and so prove nothing about what a signed-in attacker can reach; that is what an external penetration test is for, and none has been done. It does not test anything that writes: rotation, the panic button, audit streaming, builds and runs are covered by the API's own tests on an in-process cell, not live.

## What is not covered yet

The [threat model](https://docs.qaldy.com/security/threat-model/) lists each control with a status. Rows marked *planned* have no proof because the control is not built, for example run-time enforcement of the lethal-trifecta rule for AI runs, or per-run egress caps. Rows marked *accepted-risk* say why.

## Run them yourself

The proofs are a script in the repository (`pnpm test:trust`), and the model's own checks run in CI on every change: the authorization model tests, the audit-chain tamper test, the shared sealing vectors, the policy tests, the builder's static checks, and the gate's and the runtime host's test suites. The repository is private during the pilot, so for now that means asking us. We publish the result of the end-to-end run in the ledger above, with the commit, so that you can see when it is stale.