Specification Elicitation and Validation

Specification Elicitation and Validation

If proofs are cheap and specs are expensive, then specs are the bottleneck. Every widget in this document terminates in a spec: a verified sampler is verified against some statement of what a sampler should do, an OCI runtime is hardened against some threat model, an IAM policy is checked against some notion of least privilege. The spec is where human intent meets machine-checkable formalism, and it is the part that no proof oracle can write for you — or rather, if a proof oracle writes it for you, you have quietly handed over the thing you were trying to keep.

Two subproblems:

• Elicitation. Getting the spec out of the stakeholder’s head and into a formal language, without losing the parts they could not articulate. The classical software-engineering requirements-gathering literature is relevant but insufficient — we need elicitation techniques that produce artifacts a kernel can consume, not prose a PM can sign off on.
• Validation. Convincing yourself that the spec you wrote is the spec you meant. A proof of P against the wrong P is worse than useless: it launders a bug into a theorem. The property-based testing tradition [1] and the spec-mining tradition [2] are the two complementary handles we have on this — the first forces you to execute the spec against concrete inputs, the second infers candidate specs from observed behavior for the human to ratify or reject.

TODO: discuss the relationship to § — if the proof substrate is itself opaque, spec elicitation becomes unsolvable rather than merely hard, which is why we treat that as a separate enabler.

TODO: discuss differential specification (two independently elicited specs, checked for agreement) as a validation technique.

Solution/project Sketch

TODO: flesh out. Candidate directions: interactive spec-synthesis from examples, lightweight formal methods for spec sanity-checking, spec-level mutation testing, and human-factors work on what kinds of formal notation domain experts can actually read and write.