---
name: Formal Methods & Quality Assurance
description: Raise software quality with the rigorous end of the toolbox — static analysis, property-based and contract testing, and lightweight formal specification where correctness really matters — plus a QA strategy that puts effort where the risk is, so critical logic is verified rather than just spot-checked.
audience: engineer · QA/quality lead · founding engineer
---

# Formal Methods & Quality Assurance

## What this is
A method for engineering correctness: applying static analysis, property-based testing, contracts/assertions, and — where the cost of a bug is high — lightweight formal specification and model checking, all wrapped in a QA strategy that concentrates rigor on the risky, high-consequence parts of a system.

## What this is NOT
- **Not a proof of bug-freeness.** Even formal methods verify a *model* against a *spec*; the skill is explicit that "verified" means "against these assumptions," and testing shows presence of bugs, not their absence.
- **Not gold-plating everything.** Full formal verification is expensive and reserved for genuinely critical logic (money, safety, concurrency, auth); most code gets proportional rigor, not maximal.
- **Not a substitute for a specialist** on safety-critical certification (avionics, medical) or cryptographic verification.

## When to use
A quality strategy for a codebase; hardening critical logic (payments, permissions, state machines, concurrency); adding static analysis and property-based tests; specifying and model-checking a tricky protocol or invariant; deciding where verification effort actually pays off.

## Operating principle
Rigor follows risk. Spend verification effort where a bug is expensive and hard to catch by example (concurrency, money, auth, invariants) and use lighter checks elsewhere — and always state what a "pass" actually proves and what it assumes.

## Capabilities
- **Static analysis & type rigor** — Goal: catch classes of bug before runtime. Method: strict compiler/linter settings, type-driven design (make illegal states unrepresentable), taint/dataflow analysis for security-relevant paths, treat warnings as errors. Output: a static-analysis setup + a list of eliminated bug classes. Quality bar: whole categories of error are made impossible or caught at build, not left to tests.
- **Property-based & contract testing** — Goal: test the space, not just examples. Method: property-based tests over invariants (round-trips, idempotence, ordering), pre/post-condition contracts and assertions, fuzzing on parsers/inputs, coverage of edge cases the author didn't imagine. Output: property tests + contracts on critical modules. Quality bar: invariants are tested across generated inputs, not three hand-picked cases; a found counterexample becomes a committed test.
- **Lightweight formal spec (where it counts)** — Goal: verify the hard part. Method: specify a critical protocol/state machine (e.g., in a model checker), check safety/liveness properties, and reconcile the spec with the implementation. Output: a spec + checked properties + the assumptions. Quality bar: the verification names its model and assumptions explicitly; "verified" is never presented as "cannot fail."

## A worked example
"Our payment state machine occasionally double-charges." → Rather than adding more example tests, the skill specifies the state machine and model-checks the invariant "no charge without a completed authorization and no duplicate on retry," finding a race in the retry path; the fix is verified against the spec, a property-based test encodes the invariant for CI, and the write-up states plainly that this verifies the model under its concurrency assumptions — not a universal guarantee.

## Guardrails & escalation
Safety-critical certification (DO-178C, IEC 62304) → qualified specialists. Cryptographic/protocol verification → security/formal specialists. Anything where "verified" could be over-read → the assumptions are stated and, if high-stakes, independently reviewed. Rigor is proportional and honest.

## References
Static analysis and type-driven design; property-based testing (QuickCheck lineage), fuzzing, contracts/design-by-contract; model checking (TLA+, Alloy) for critical invariants; the principle that testing shows presence, not absence, of bugs (Dijkstra). Match rigor to consequence.