[tobyhede]

Requested by Toby

Stacked on #490, which adds the Quint agent skills, the mise tasks and their docs. Merge #490 first.

This is a proof-of-concept formal model, in Quint, of how Proxy decides to map, forward or refuse each statement.
It checks that plaintext never reaches an encrypted column, except when the client uses UNSAFE_DISABLE_MAPPING.
The model is design-level only: it changes no production code, and no Rust code is tested against it yet.

Start with specs/quint/routing/requirements.md, which covers the scope, assumptions, properties, findings and open decisions, and maps each model element to its Rust code.
verification.md has the exact results.

What it models

• The refuse-by-default Frontend::route from refactor(proxy): route each statement through one refuse-by-default decision #484, including may_fall_back, the unresolvable-table refusal (fix(proxy): refuse writes to a table Proxy cannot resolve #486), the simple Query batch rule, and the COPY ... FROM and nested-write refusals from fix(proxy): refuse COPY FROM into encrypted columns, check statements after COPY FROM STDIN #488.
• The Bind settings check (PreparedSettingsChanged), gated by requires_schema.
• One connection running simple Query batches, Parse, Bind/Execute, Close, transactions and UNSAFE_DISABLE_MAPPING.
• Both values of mapping_errors_enabled.
• Optionally, another connection committing DDL that changes whether a column is encrypted.

Results (Quint 0.33.0, TLC, exhaustive for each finite instance)

• S1–S3 hold as built, including with UNSAFE_DISABLE_MAPPING and concurrent DDL.
  With a stable schema, Proxy's routing alone keeps them true, even with PostgreSQL's domain check switched off.
• TLC catches each of eight injected faults (M1 to M8), including no batch rule (main's behaviour before refactor(proxy): route each statement through one refuse-by-default decision #484), no Bind settings check, and no COPY ... FROM refusal.
• Every action has a witness that only it can reach, and simulation fails if any witness is reached in 0 traces, so a dead action fails CI.

Findings to confirm against real Proxy before acting

These are recorded as expected counterexamples, so CI fails if one stops reproducing.

• F3 (retracted): the first version of the model left out the Bind settings check (PreparedSettingsChanged), so it reported a plaintext path that Proxy does not have. The model now includes the check, and mutation M4 covers it.
• F1: routes go stale under concurrent DDL. Prepared statements are routed once, at Parse, transactions pin the schema, and DDL from elsewhere is published only by the periodic reload. Only PostgreSQL's type and domain checks stop the plaintext write.
• F2: DO, CALL and SQL EXECUTE are opaque to Proxy, so nothing in routing stops them writing plaintext. COPY ... FROM is no longer part of F2: fix(proxy): refuse COPY FROM into encrypted columns, check statements after COPY FROM STDIN #488 refuses it.

PostgreSQL's domain check should reject the value in every case, so none of these is a confirmed leak. Each would need a failing test first.

Requirements changes for review

No property (S1 to S4) changes. These assumptions change:

• A3 now covers only DO, CALL and SQL EXECUTE; COPY ... FROM and nested writes are modelled.
• A5 is documented as an over-approximation: publication follows the commit, and DDL from elsewhere waits for the periodic reload.
• New A6: a nested write takes no parameters, so a nested write prepared with mapping disabled carries values sent with mapping disabled.
• New decision D4: Bind and Execute stay one step.

Tooling

• specs/quint has a pinned package-lock.json. check.sh covers typecheck, scenario tests, simulation with every witness required to be reached, TLC and mutations.
• .github/workflows/quint.yml runs only on changes under specs/quint. It isn't a required check, and a full run takes about 7 minutes.
• npm audit flags adm-zip, which Quint uses only to unpack its own Apalache download, as the README notes.

Acknowledgment

By submitting this pull request, I confirm that CipherStash can use, modify, copy, and redistribute this contribution, under the terms of CipherStash's choice.

---

Generated by Claude Code

[cipherstash-agent]

Review attestation

Source: Claude Code, /code-review medium plus company-skills:cross-check-review-findings (loaded from cipherstash/skills). Reviewed head 1d3997f.

Result: No critical or blocking issues. 3 minor findings, inline.

Cross-check: The PR had no prior reviews, review threads or comments, so all 3 findings are new.

What I checked

• The model against requirements.md: properties S1–S4, assumptions A1–A5 and findings F1–F3.
• The four mutation patterns in check.sh. Each from string occurs once in routing.qnt.
• The scenario tests' expectations traced against the actions.
• The workflow and tooling files.

Not done: I did not run Quint or TLC. I did not compare the model with Frontend::route or the other Rust sources it cites (#484 and related). It is a design-level model with no Rust adapter, so that comparison is the open risk, as F3 showed.

The lockfile was skimmed, not audited.

---

Generated by Claude Code

[cipherstash-agent]

Minor (stale comment). This says "S4 (open decision D1)", but requirements.md records D1 as decided on 2026-10-25 (S4 is not a requirement). Suggest "S4 (not required; D1 decided)" so the model and the contract agree.

Source: specs/quint/routing/requirements.md (Decisions, D1; Properties, S4) at head 1d3997f.

---

Generated by Claude Code

[tobyhede]

Fixed in 8791e17: the comment now reads "S4 (not required; D1 decided)".

---

Generated by Claude Code

[cipherstash-agent]

Minor (hardening). The workflow sets no permissions:, so the job gets the repository's default GITHUB_TOKEN scope. It only checks out and runs checks, so a top-level permissions: contents: read is enough and keeps the token minimal.

---

Generated by Claude Code

[tobyhede]

Fixed in 8791e17: the workflow now sets a top-level permissions: contents: read.

---

Generated by Claude Code

[cipherstash-agent]

Minor. If this grep matches nothing (for example Quint changes its output wording), set -e and pipefail end the script here with no FAIL: message, even though TLC passed. Add || true, or fail explicitly with the captured output, so a wording change is not mistaken for a model failure.

---

Generated by Claude Code

[tobyhede]

Fixed in 8791e17: the summary grep now ends with || true, so if Quint changes its wording a passing check still passes.

---

Generated by Claude Code