Prove the Spec Before You Write the Code with symspec

A solver can prove a conflict; review supplies context. #

The premise is that a contradiction between two requirements is a logical fact, so logic should decide it. symspec runs a forced pipeline, parse → lint → check → certify, and the order carries weight: a statement that fails an earlier surface stage is excluded from the formal stage, because feeding unparsed text into an SMT encoding is unsound, and the exclusion is reported so nothing vanishes silently.

The parse step is a regex-first ladder that escalates only as far as it must. Clean EARS sentences never load a model; a natural-language parser (wink-nlp) loads lazily only on a genuinely hard clause; a sentence that still will not yield full slots returns a structured error with a rewrite suggestion, never a low-confidence guess. What survives becomes Boolean atoms through one pure atomize function with a deliberately conservative normalization: lowercase, strip leading articles, collapse whitespace. It does not stem or lemmatize, every atom is scoped to its system so identical text under two systems stays two distinct atoms, and a seed antonym table of 15 pairs unifies polar opposites like grant and revoke. Each requirement then encodes as a guarded implication and goes to the solver.

The whole loop on two requirements that disagree looks like this:

$ symspec add reqs.symspec.json --pattern event-driven --system "auth service" \
    --response "grant access" --trigger "the user submits valid credentials"
$ symspec add reqs.symspec.json --pattern event-driven --system "auth service" \
    --response "revoke access" --trigger "the user submits valid credentials"
$ symspec check reqs.symspec.json

grant access and revoke access resolve to the same atom at opposite polarity, so the solver returns unsat, and check emits a FND_CONTRADICTION naming exactly the two culprit IDs with the atom table and the minimal unsat core as evidence. The exit code is the gate: 0 clean, 1 an error-severity finding is present, 2 an operational failure. That is the entire pass-fail contract an editing loop or a CI job needs.

The propositional check is one tier of several, and the others close the gaps it cannot see. A numeric tier lifts (quantity, comparator, value, unit) from the text, normalizes units, and proves jointly-unsatisfiable bounds over linear arithmetic, so latency ≤ 2000ms against latency > 3000ms surfaces as a proven conflict between two numbers the eye would never line up. A temporal tier maps EARS patterns to linear temporal logic and lowers them to a bounded finite-trace encoding, catching “eventually open the valve” against “never open the valve.” Deterministic ambiguity detectors flag vague terms, un-parenthesized and/or scope, and a pronoun with two possible antecedents. Each of these returns an identifier and a proof obligation rather than an adjective.

Built for the agent to drive #

The mechanical check is half the tool. The other half is the discovery that a verifier only earns its place if the thing writing the spec can operate it without trial and error, and an agent driving a CLI has exactly two failure modes: it cannot tell whether it succeeded, and it has to guess what the tool accepts. symspec closes both.

The first move is a self-describing manifest. symspec manifest emits, as one JSON blob, every command, every argument schema, every stable code, the closed set of envelope types, the scope disclosure, and a live report of which backends are installed on this machine. An agent fetches it once and decides before it invokes, so its first attempt is already an informed one.

The second move is that every command answers in the same envelope shape: success is { apiVersion, type, data }, failure is the same superset plus code and a suggestions array. The agent branches on a code, never on an English sentence. Those codes are three exported enums, append-only and guarded by a snapshot test so they cannot be renumbered out from under a caller: 21 operational ERR_* codes, 24 INCOSE GTWR_* lint codes, and 26 finding FND_* codes across 19 commands. When a value is rejected, the error names the exact allowed set and the offending character span; when a rule fires, the finding carries a concrete rewrite.

The largest lever is authoring in one atomic move. symspec apply folds a whole batch of operations, adds and edges and updates together, into a single transaction with stable human keys like G1 or AUTH-3 that resolve forward within the batch. It all lands or none of it does. There is a --dense mode that strips output to the minimum tokens while validating against the identical schema. The zero-flag default is already machine-readable, so an agent never needs a flag to get parseable output, and the entire surface is an importable TypeScript library as well as a command line. This is a general lesson that outlived the project: a tool meant for an agent should publish its own contract, speak one envelope, and let the caller branch on codes.

It refuses to claim more than it proved #

The feature I am most attached to is the one that makes symspec sound less impressive. The propositional tier is sound modulo atomization: every conflict it reports is a genuine logical conflict of the requirements as atomized. The flip side is that because two paraphrases become two distinct atoms, a real conflict can hide behind atoms that never matched, so a clean check means “no conflict was proven,” never “the spec is proven consistent.” symspec says exactly that, in the manifest, in machine-readable form, with the wording pinned by a schema so the disclosure cannot drift as the code changes.

This matters most where silence looks like a pass. When the formal tier compares zero pairs because no two requirements shared an atom, the run reports pairsChecked: 0 and withholds the reassuring green. A less careful reader would assume the spec had been cross-checked when nothing was. The learned tier holds the same line by splitting propose from decide. Embeddings from a pinned local model run once and only ever propose a glossary merge for a paraphrased pair; a committed glossary in the document, reviewed by a human or an agent and stored in git, is what decides, and the verdict path reads that glossary, never the model. Determinism is never traded for recall: a verdict-eligible finding must recompute bit-for-bit from the document, the committed glossary, and the pinned model, and everything fuzzier is downgraded to info and proposes.

Even the Lean 4 certification tier, the most authoritative-sounding thing in the box, undersells itself on purpose. certify generates a batched core-Lean file, runs it through the kernel, and retains a re-checkable artifact with #print axioms provenance. Its success message states plainly that the broader-scope theorems are still placeholder True and that the SMT tier is the gate that counts. A tool that tells you which of its guarantees carry weight and which are scaffolding is rare, and it is the difference between a verifier and a comfort blanket.

The tool got better by being driven by an agent #

The clearest evidence that agent-first is a design constraint is that an agent found the flaws in the interface by living in it. Early on, a Claude Code agent authored a 42-requirement schedule-management spec end to end: linted clean at error severity, semantic tier run, certified in Lean. It succeeded, and the field report it left behind was a catalog of friction. Because every operation was one process, it made roughly 150 subprocess calls and wrote a driver script to survive them. Because the tool addressed requirements only by UUID, it maintained a label-to-UUID sidecar file for the whole session. Its check returned 4 real errors buried under nearly two hundred style warnings that it triaged and waived by hand, with nothing recording that it had reviewed them, so the next run would re-emit the same wall. And its formal tier reported pairsChecked: 0, which it noticed only because it printed the field.

The report ended in a ranked wishlist. Most of it is now shipped, and the left column is the primitive that closed each gap:

A later agent, given the rebuilt tool, described the difference from the inside: it authored a 25-requirement architecture spec in a single atomic apply, waived 122 intentional style findings with recorded reasons so the baseline read as triage, kept one genuinely-similar pair distinct on purpose after the semantic tier flagged it, and kernel-checked the whole thing in Lean. Its verdict was that this was the first spec tool it had used that was built for an agent to drive, and that it never had to parse prose to find out whether it had succeeded.

This is where the frontier points. As base models get better at generating code, the leverage stops being in the generation and moves to two places the model cannot supply for itself: an external, deterministic check that can be wrong out loud, and an interface clear enough that the model knows what the check did and did not do. “The model proposes, the solver disposes” describes the shape of the whole field’s recent gains, where external verification buys far more than any amount of a model grading its own work. symspec is one instance of it, aimed at the layer where software goes wrong first.

Where to start #

Take a spec an agent wrote for you, one you would otherwise skim and approve. Write the requirements in EARS, run symspec check, and read the findings it returns as identifiers you can act on. If it proves a contradiction, you found a bug before a line of code existed. If it proves nothing, notice that it told you so plainly, and that a clean run is a floor rather than a certificate. Then point your own agent at the manifest and let it drive. The check is mechanical, the interface is built for the driver, and the tool claims only what it proved.

Check the spec with a solver, and let it tell you plainly what it proved. The code you generate from a spec that was never checked is the code most likely to be wrong.