pstack-create-formal-verification-skill
Create a formal verification skill
Verify one property where a defect would harm users and tests rarely reach the failing case. Leave a project-local skill that lets the next agent check a relevant change without learning the verification language. This task generates verification artifacts. Report product defects separately and change product code only within an existing grant.
1. Choose the property from the code
Answer from the codebase, and ask the user only what you cannot observe. Start with the user's named area or bug. Otherwise inspect the repository for a consequential promise involving concurrency, retries, state machines, parsing, unsafe code, or another difficult case. Choose the strongest useful target rather than the easiest demonstration. State the property and the harm from violating it in one plain sentence each.
Complete when one target has source locations, a precise property, and an observable failure condition.
2. Let the question choose the tool
Inspect available tools and the repository's constraints. Choose a model checker, proof assistant, SMT-backed verifier, or other suitable tool at the lowest useful cost. Event ordering often suits a small design model. Memory safety, overflow, or data-structure invariants can suit a verifier that checks the code. If no verifier supports the language, say so and test the real code with generated inputs; distinguish that evidence from a formal proof. A property required at every size can need a proof. For concurrent or distributed designs, consider TLA+ alongside tools already used by the repository.
Prefer existing tools or a project-local installation developers can rerun. Record its reproducible version, installation command, verification command, and expected cost. Use current primary documentation for any unfamiliar tool. Explain why the tool answers this question.
Complete when the chosen tool runs locally. If a required tool cannot run, skip to step 6 and hand off a draft naming the missing prerequisite and unverified scope.