Skip to content

yuxuandexter/vstack

v0.1.0MIT

Formal verification workflows for concurrent, distributed and systems software.

vstack-mode

Run the Verification Stack for a concurrent, distributed or systems-software property, from source archaeology through calibrated models, red team, proof and maintained regression. Use for /vstack-mode or an end-to-end verification workflow.

vstack-s0-decompose

Map a pinned system into control, data and boundary views and build evidence-backed historical anchors before verification.

vstack-s1-select

Choose verification tools and assurance tiers per property using state, scale, ownership and consequences.

vstack-s2-spec

Derive observable contracts, calibrate both legal and illegal behavior, then freeze owner-approved specifications and configurations.

vstack-s3-model

Construct state transitions or computation descriptors from pinned code without hiding interleavings or unchecked assumptions.

vstack-s4-calibrate-tv

Calibrate buggy/fixed/ablated behaviors and validate model conformance using real traces, witnesses and explicit mismatch triage.

vstack-s5-redteam

Audit calibrated verification through independent attacks on fidelity, property/gate strength and scope extrapolation.

vstack-s6-hunt-fix

Search within a trace-validated model scope, classify counterexamples and validate fixes in both the model and real code.

vstack-s7-prove

Prove pinned design-model properties in one shared TLAPS module tree after invariant discovery, calibration and trace alignment.

vstack-s8-package-maintain

Package verified scope into a project-local five-step regression skill and keep it aligned with future code revisions.