Pilot: formal verification (TLA+ / Lean) of the sync engine and other data-loss-critical state machines

[padak]

Summary

Evaluate formal methods (Lean 4 proofs, TLA+ model checking) for the parts of kbagent where a logic error means lost or duplicated production data. Inspired by Anthropic's use of Lean/TLA+ on the Claude Agent SDK state machines: extract a small model from real code, prove invariants / search for counterexamples, replay every counterexample against the real code as a failing test, then fix.

This is deliberately targeted, not "verify the whole CLI".

Why kbagent is a partial fit

Most historical kbagent bugs are not internal-logic bugs a model would catch:

• Misunderstood Keboola API semantics (DELETE on a trashed config purges permanently, notification ?event= is silently ignored, Metastore opaque 401). A model only proves properties of the model; if it encodes the API as wrongly as the code does, the proof passes and the bug stays.
• Documentation / plugin drift (CLAUDE.md convention v0.6.0: Branch lifecycle management + security hardening #17).
• Windows vs POSIX OS behavior.

Where it does fit (ranked)

1. Sync engine (pull / push / diff) -- a real three-way state machine (local tree / manifest baseline / remote) with branch trees and ignored components, and a documented history of data-loss bugs: delete-dir-then-push destroyed production configs (sync: ignore keboola.mcp-server-tool workspace records like keboola.sandboxes — and manifest ignoredComponents is never read #689), scaffold push created 34 duplicates (config new --output-dir --push writes a scaffold without the created config ID → duplicates on next sync push #644), permanent phantom drift (sync push stamps pull_config_hash from disk while diff compares an API-derived hash — every pushed config stays "REMOTE MODIFIED" forever (mirror of #466) #686), cross-branch tree mixing (sync: production diff/push after 'sync pull --branch' flags the whole orphaned main/ tree as added (mass-duplicate risk) #649). Each is expressible as an invariant, e.g. push never deletes a remote config the user did not deliberately delete locally; pull --force never silently discards a local modification.
2. Destructive operations under network failure (TLA+) -- config delete locate-first guard, notification replace-recipient create-then-delete, non-retried project create, job run idempotency. Question: can any interleaving of timeout / retry / concurrent run lose or duplicate a resource?
3. Cross-process concurrency on local state -- auth.json has a real cross-process lock; config.json uses a weaker helper. Parallel agent invocations + serve + scheduler are the classic interleavings tests miss. (No known bug -- a place to look.)
4. Permission engine -- pure function with safety properties (--deny-destructive never permits a destructive op; adding a deny never grants). Property-based tests (Hypothesis) likely give the same confidence far cheaper than Lean.

Not worth it: HTTP client wrappers, output formatting, self-update, merge-request derived states (truth lives server-side).

Risks

• Model drift: Lean/TLA+ cannot be extracted from Python; the model is a hand-written abstraction. The durable artifact is the regression tests born from counterexamples, not the proofs.
• Human review is the bottleneck: someone must confirm the model matches both the code and live API behavior.

Pilot plan (sync engine)

1. Derive invariants from the sync bug history and current code.
2. Model push/pull/diff classification in TLA+ (TLC counterexample search); prove the pure classification properties in Lean where it is cheap.
3. Replay every counterexample as a pytest against the real code.
4. Reproduced -> fix + regression test in a normal PR. Not reproduced -> tighten the model.

Success criterion: number of counterexamples that reproduce as failing tests against real code. Zero reproducible findings -> stop, fall back to property-based testing. The model is committed as documentation only, not a CI gate.

[padak]

Pilot results + handover

TL;DR: formal models of the sync engine found 11 findings, 10 reproduced against the real code. The 4 most severe (data loss / duplication) are fixed in draft PRs. Nothing is merged yet. Two findings need an owner decision (G, H).

What was verified

• TLA+ (formal/sync/tla/): TLC over a finite model (2 branches, 2 local trees, 4 config ids, content versions 0-2, one ignorable component). 13 invariants, ~153k distinct states per run, depth MaxSteps=4.
• Lean 4 (formal/sync/lean/): the pure decision functions (diff classification, pull per-config decision, push create/update/delete). 35 theorems, 0 sorry, standard axioms only. Every def cites the Python file:line it mirrors. A false property is kept as a proven negation with a concrete counterexample.
• Replay (tests/test_sync_formal_counterexamples.py): one test per finding, driven through the real SyncService with a mocked client. A still-open bug is xfail(strict=True); a fix PR removes the marker.
• Different tools caught different bugs: A was found independently by both, B only by Lean, D and F only by TLC.
• The models are documentation, not a CI gate. How to run them: formal/sync/README.md.

Findings

ID	Finding	Severity	Status
A	Config deleted in the UI and re-created under the same name -> pull deletes the dir it just wrote -> the next push DELETEs the live new config	HIGH	fixed in #796 (draft)
B	pull / pull --force compare only _config.yml: edits in transform.sql, code.py, _description.md or row files are silently overwritten, with no SYNC_CONFLICT	HIGH	fixed in #795 (draft)
C	Remote delete + local edit -> pull deletes the locally edited dir without a conflict	HIGH	fixed in #796 (draft)
D	sync push --branch dev (promoting main/) creates another dev copy of each prod config the dev branch lacks, on every push	HIGH	fixed in #794 (draft)
E	An untracked file carrying a config id (scaffold / adopted) is compared 2-way, so push overwrites UI edits; two copies with the same id -> last one wins	MED	open, recommended next
F	After a push aborted with ENCRYPTION_FAILED, the retry duplicates the configs the aborted push had already created	MED	open, recommended next
G	sync push deletes remote configs without --force, although the help text says --force gates deletion (deletes are soft, restorable from trash)	MED	owner decision
H	A config deleted remotely by another actor is silently re-created by the next push under a new id	MED	owner decision
I	mv of a config dir becomes a remote DELETE + CREATE under a new id	LOW-MED	open
J	pull --branch dev reports untouched prod configs as "removed" in details[] (nothing is deleted on disk)	LOW	open
K	A cosmetic local edit (raw vs normalized hash) keeps plain pull from ever applying a remote change	-	documented conservative behavior, kept as a regression guard

PRs

PR	Scope	Review	CI
#793	Pilot: models + replay tests; no production code	-	green
#794	D, stacked on #793	0 blocking	none yet (see merge order)
#795	B, stacked on #793	0 blocking	none yet
#796	A + C, stacked on #793	0 blocking	none yet

The three fix PRs passed make check locally, but CI does not run on them while their base is not main.

Non-blocking review notes to resolve before merge:

• fix(sync): pull never deletes a dir it wrote or a locally edited dir (#792 A, C) #796:
  • NB-1: C now keeps a locally edited dir whose remote was deleted, so the next plain push re-creates it under a new id. That is finding H, now more reachable.
  • NB-2: A's rename-back of the temporary suffixed dir is reported as "renamed", indistinguishable from a real remote rename, and has no dedicated regression test.
• fix(sync): promoting main/ to a dev branch is idempotent (#792 D) #794: pre-existing (I8): after a promote push, the file in main/ gets the dev config id, so offline sync status marks the dev entry deleted and the prod entry modified. The PR body understates this.
• fix(sync): pull protects local edits in companion files, not only _config.yml (#792 B) #795: companion-file comparison hashes raw bytes with no CRLF normalization, now on every pull. This matches diff/push/status, but is worth a gotchas note given the Windows line-ending history.

Merge order

1. Merge test(sync): formal verification pilot of the sync engine (#792) #793.
2. Retarget fix(sync): promoting main/ to a dev branch is idempotent (#792 D) #794, fix(sync): pull protects local edits in companion files, not only _config.yml (#792 B) #795 and fix(sync): pull never deletes a dir it wrote or a locally edited dir (#792 A, C) #796 to main (this triggers CI) and merge them one at a time. All three touch gotchas.md, sync-workflow.md and the findings table in formal/sync/README.md, so expect small doc conflicts. Each fix PR removes only its own xfail markers.
3. No version bump or changelog entry in any of them. The docs use (since vNEXT) for the release PR.

Decisions needed from the owner

• G: fix the help text to match today's behavior (plain push deletes), or actually require --force for deletes? The second option is a breaking change for scripted sync push.
• H: when a tracked config no longer exists remotely, should push re-create it (today, silently), warn and re-create, or refuse with a conflict until pull or an explicit flag? The fix(sync): pull never deletes a dir it wrote or a locally edited dir (#792 A, C) #796 fix for C makes this path more common, so the decision should land before or with fix(sync): pull never deletes a dir it wrote or a locally edited dir (#792 A, C) #796.

Suggested next steps

1. Fix E and F; both have strict-xfail tests ready.
2. Once G and H are decided, update the tests to the chosen behavior.
3. When a fix lands, re-run TLC (formal/sync/tla/run_all.sh) after updating the model to the fixed code. The models were not updated in the fix PRs, so TLC still flags A–D.
4. Possible follow-ups outside sync, from the original assessment: destructive ops under network failure (TLA+), and the cross-process lock on config.json.

Toolchain

• TLA+: tla2tools.jar v1.8.0 plus Java 17+.
• Lean 4.34 via elan (core only, no Mathlib); lake build in formal/sync/lean/.