How We Work

Why spec-first

Most AI systems are built without a behavioral specification. You build something, test some examples, it seems OK. But "seems OK on the examples you tried" is not the same as "behaves correctly." Without a spec, you can't define what correct means — so you can't verify it, and you can't know what you don't know.

Coding agents make this worse, not better. They produce plausible code faster than anyone can review it, and plausible is exactly the failure mode example tests miss. The bottleneck has moved from writing code to knowing whether it is right.

Spec-first forces the question before any code is written: what exactly must this system do? Stated precisely, that question becomes testable. Testable means verifiable. Verifiable means you ship with confidence instead of hope.

How spec-first works

You write the invariants first — the behavioral properties that must hold for all inputs of a given shape, not just the ones you thought to try. Then you derive tests from those invariants. Then you implement until the tests pass.

Property-based testing is the main tool for this: instead of writing assert f(3) == 9, you write assert f(x) == f(-x) for all integers x. The framework generates inputs automatically, including edge cases a human would never write, and shrinks failures to the minimal counterexample.

Then you check the tests themselves. Mutation testing introduces deliberate bugs and confirms the suite catches them; a suite that passes against broken code is not a specification, it is decoration.

The lineage is John Hughes and Koen Claessen's QuickCheck, developed at Chalmers University of Technology. Hughes' How to Specify It! (2020) is the canonical reference. The founder's MSc is from the same program.

What a property looks like

A concrete instance, using SqlProof against a two-table schema. The property is a sentence a product owner could read: no line item may ever reference an order that does not exist. The test does not pick examples; it states the rule and lets the tool search for a violation.

schema.sql

CREATE TABLE orders (
  id SERIAL PRIMARY KEY,
  customer_id INTEGER NOT NULL,
  total NUMERIC(10,2) NOT NULL CHECK (total >= 0)
);

CREATE TABLE line_items (
  id SERIAL PRIMARY KEY,
  order_id INTEGER NOT NULL REFERENCES orders(id),
  quantity INTEGER NOT NULL CHECK (quantity > 0),
  price NUMERIC(10,2) NOT NULL CHECK (price > 0)
);

test_orders.py

from sqlproof import SqlProof, sqlproof

proof = SqlProof.from_schema_file("./schema.sql")

# Property: no line item may ever point at a missing order.
# SqlProof generates 50 schema-valid datasets, runs the query
# against each, and shrinks any failure to the smallest one.
@sqlproof(proof, sizes={"orders": 20, "line_items": 50}, runs=50)
def test_no_orphan_line_items(db):
    rows = db.query("""
        SELECT li.id
        FROM line_items li
        LEFT JOIN orders o ON li.order_id = o.id
        WHERE o.id IS NULL
    """)
    assert rows == []

SqlProof parses the schema, orders the tables by foreign key, generates rows that honor the types and constraints, and runs the property under Hypothesis. When it fails, you get the smallest dataset that breaks the rule, not a stack trace from production.

How we apply it

What an engagement looks like

We start by writing the spec — the behavioral invariants your AI system must maintain. Then we build tests that enforce them and run mutation testing to verify the suite would catch real failures. The output is a spec and a test harness you own, not a report.

Engagements are scoped, time-bounded, and end with a handoff. We take on a small number at a time.

What we do not do: open-ended staff augmentation, prompt tuning without a test oracle, or AI strategy decks. If the work cannot be stated as something checkable, it is not a fit for us.