Conversation
TLA+ model (TLC) and Lean 4 model of the sync pull/diff/push decision logic, plus one pytest per consolidated finding (A-K) replayed against the real SyncService. Reproduced bugs are strict xfail tests; remove the marker when the fix lands. Models are documentation, not a CI gate.
keboola-pr-reviewer-bot
left a comment
keboola-pr-reviewer-bot
left a comment
There was a problem hiding this comment.
Verdict: auto_approve (risk 1/5) · profile _default
Test-and-docs-only formal-verification pilot with zero production runtime changes; safe to auto-approve.
![devin-ai-integration[bot]](https://avatars.githubusercontent.com/in/811515?s=60&v=4){kind=small}
| java -XX:+UseParallelGC -cp ~/tools/tla/tla2tools.jar tlc2.TLC -workers auto -deadlock \ | ||
| -dumpTrace json $N.json -metadir "states_$N" -config $N.cfg SyncEngine.tla > $N.log 2>&1 || true | ||
| rm -rf "states_$N" | ||
| grep -E "violated|No error|states generated|distinct states|Error:" $N.log | head -5 |
There was a problem hiding this comment.
🟡 Model-checker errors return success
When TLC fails before checking an invariant, run_one.sh discards its exit status. The final log-filter pipeline still returns zero, so verification runs can pass without checking the model.
Learn more
TLC uses a nonzero status for invariant violations as well as tool and model errors. The runner currently ignores all such statuses, then returns the status of head, which succeeds even if the log contains an error or no result. That makes a missing jar, an invalid model, or an incomplete run indistinguishable from a completed check to a caller using the script's exit status.
Example: With an invalid tla2tools.jar path, Java writes an error to the log and exits nonzero. run_one.sh prints the error but exits zero, so run_all.sh can finish successfully without running TLC.
Recommended fix: Preserve TLC's status and explicitly classify its log as a completed proof, an expected invariant counterexample, or an execution/model failure. Return nonzero for the last case, and propagate it from run_all.sh.
Was this helpful? React with 👍 or 👎 to provide feedback.
| { [kind |-> "deleted", id |-> id, path |-> st.mn[id].path, trk |-> TRUE, | ||
| comp |-> st.mn[id].comp, base |-> st.mn[id].base] : id \in Deleted(st, b) } |
There was a problem hiding this comment.
🔍 Deletion invariant assumes a path absent from real diffs
I2_DeleteOnlyUserRemoved checks deleted changes against userDel using their path. Real compute_changeset emits those changes with path="". The model therefore tests a richer change record than the service receives; keep the manifest path as separate ghost state if this invariant needs it.
Was this helpful? React with 👍 or 👎 to provide feedback.
| sql_client_pull("SELECT 100;") # remote changed the SQL in the meantime | ||
| w.svc.pull(alias="prod", project_root=w.root) | ||
|
|
||
| assert "SELECT 42" in sql_file.read_text(), ( |
There was a problem hiding this comment.
🔍 Force-pull SQL behavior remains untested
The companion-file finding covers plain pull and --force, but the regression test calls only plain pull. Because --force has a separate conflict guard, add a case that exercises it after local and remote SQL edits.
Was this helpful? React with 👍 or 👎 to provide feedback.
This branch has not been deployed
2 participants
Summary
Pilot for #792: formal verification of the sync engine (pull / diff / push).
formal/sync/tla/: TLA+ model checked with TLC (2 branches, 4 configs, ignorable component, ~153k states per run).formal/sync/lean/: Lean 4 model of the pure decision functions: 35 theorems, 0sorry, standard axioms only. False properties are kept as proven negations with concrete counterexamples.tests/test_sync_formal_counterexamples.py: one test per finding, replayed against the realSyncServicewith a mocked client. Reproduced bugs arexfail(strict=True). A fix PR removes the marker.The models are documentation, not a CI gate. See
formal/sync/README.mdfor how to run them.Findings (all reproduced against real code except K)
_config.yml: edits intransform.sql/code.py/_description.mdare silently overwritten, with no SYNC_CONFLICTsync push --branch dev(promotingmain/) creates another dev copy of each prod config dev lacks, on every pushsync pushdeletes remote configs without--force, although the help text says--forcegates deletion (deletes are soft, to trash)mvof a config folder becomes remote DELETE + CREATE under a new idpull --branch devreports untouched prod configs as "removed"No production code changes in this PR. Fixes follow in separate PRs.
Test plan
pytest tests/test_sync_formal_counterexamples.py: 1 passed, 10 xfailedruff check/ruff format --checkclean;lake buildOK