Add Quint tooling, modeling skills, and mutation cursor spec - #233
Merged
Conversation
Provide reusable Quint language, modeling, and spec-execution guidance with runnable examples for formal verification work. Package the Quint CLI and language server in the Nix development environment so the new skills and specifications can be typechecked and explored reproducibly. Add a bounded mutation-cursor model covering revision-checked observations, hook replay identity, scope attribution, contention, failures, recovery, and stale-attempt rejection, with implementation refinement notes. Ignore generated Apalache output while preserving the repository's staged source artifacts. Co-authored-by: SCE <sce@crocoder.dev>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Separate database-unavailable state from durable protocol state by modeling external taint and conservative recovery baselines. Add abandoned scopes, same-actor rollover, contention rules, and safety scenarios so unobserved gaps cannot receive exclusive attribution. Co-authored-by: SCE <sce@crocoder.dev>
Track standalone scope abandonment as a durable rebaseline boundary so skipped cursor intervals cannot produce mutation evidence. Record protocol, scope, rollover, and start checkpoints to prove cursor transitions, attribution suppression, and scope preservation across recovery. Document healthy rebaseline recovery separately from taint recovery and add executable scenarios covering deferred observations and prepared-attempt rejection. Co-authored-by: SCE <sce@crocoder.dev>
Track the cursor tree and revision at scope abandonment so the model can prove that abandonment creates a rebaseline requirement without emitting mutation events. Add uniqueness and scenario coverage for the new history. Co-authored-by: SCE <sce@crocoder.dev>
Avoid the vulnerable tar 6 dependency by applying the tar 7 override during the Nix package patch phase. Refresh the lockfile so npm dependency hashes and transitive packages match the supported dependency graph. Co-authored-by: SCE <sce@crocoder.dev>
…gates Keep Quint typechecking and tests in one gate while running the safety invariant groups independently. Separate the expensive history checks with shorter trace bounds to avoid combined verification timing out while retaining all safety checks. Co-authored-by: SCE <sce@crocoder.dev>
Avoid GHSA-xcpc-8h2w-3j85 (adm-zip < 0.6.0 unbounded memory allocation on crafted ZIP central directory headers) by overriding adm-zip to ^0.6.0 during the Nix package patch phase, same pattern used for the tar 7 override. Refreshed the lockfile and npmDepsHash to match. Co-authored-by: SCE <sce@crocoder.dev>
Ensure Quint validation failures remain visible as a single workflow failure status. Add an always-running gate that skips unchanged workflows and fails when typechecks/tests or safety verification fail. Co-authored-by: SCE <sce@crocoder.dev>
Record a worktree's durable protocol state when database failure introduces external taint, and use that checkpoint to verify no durable mutation occurred. Disable abandonment while tainted and add coverage for the guarded behavior. Co-authored-by: SCE <sce@crocoder.dev>
Keep active scopes independent of harness type so starting a new scope preserves existing scopes and correctly reports subsequent mutations as contended. Remove the rollover state, transitions, safety properties, and deterministic coverage from the Quint model and align its documentation with explicit stale-session recovery. Co-authored-by: SCE <sce@crocoder.dev>
Record the observed and resulting cursor during taint recovery so external taint is cleared only after a recovery baseline is established. Clarify that taint advances the worktree revision, permits later fresh snapshots to proceed, and marks evidence as ineligible until recovery. Extend the Quint history state and recovery scenario to verify the baseline and taint-clearing behavior. Co-authored-by: SCE <sce@crocoder.dev>
Ensure recovery taint clearing is backed by a recorded cursor checkpoint at the observed tree and recovery revision. Rename directional evidence properties and replace the abandonment-specific safety check with a general preceding protocol checkpoint invariant, keeping the model's claims aligned with what it proves. Co-authored-by: SCE <sce@crocoder.dev>
Align the mutation cursor model with properties it can establish: bound the documentation's verification claim by configured depth, remove the checkpoint invariant that overstates temporal evidence, and clarify that rejected attempts do not commit evidence. Co-authored-by: SCE <sce@crocoder.dev>
CI now reruns Quint verification when the model, workflow, or Nix inputs change and uses the enabled-action `verifyStep` with representative identity domains to keep bounded checks tractable. The model separates durable protocol checkpoints from verification-only history, factors guarded actions into reusable helpers, and adds coverage for taint recovery across worktrees. Co-authored-by: SCE <sce@crocoder.dev>
Keep pull-request Quint validation within a bounded runtime by moving symbolic safety verification to a scheduled/manual workflow. Run randomized safety checks in the required workflow and update change detection and gate handling for the new job layout. This keeps deep verification available without blocking routine PR validation. Co-authored-by: SCE <sce@crocoder.dev>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.