Spec++ · Plain-language explainer

From vague requirements to proven behaviour.

This page is for engineering leaders, software engineers, and compliance teams who want to understand what working with Spec++ actually feels like. We start with a story only—no symbols you need a PhD to parse—then add one small formal example when you are ready.

The building code vs. the builder.

A building code says what must be true of every building: maximum load on a floor, how fire exits work, which materials are allowed. It does not tell the builder which tool to pick up first. The builder is free to optimise the process, as long as the finished building obeys the code.

Spec++ plays the role of the building code. AI plays the role of the builder. You write the rules that must always hold; AI generates implementations that are checked against those rules.

A tiny running example

Imagine a simple mandate rule in wealth management: no single client may own more than 10% of any fund. Today, that rule often lives in a requirements document, an email thread, and a few scattered pieces of code—none of them guaranteed to agree.

How this rule looks today.

In natural language

“For any fund we manage, no single client account should hold more than 10% of the fund’s total units. If a rebalance would cause that limit to be exceeded, it must be rejected or adjusted.”

In typical code

if client_units / fund_units > 0.10:
    raise LimitBreachError()

This line looks fine, but it hides questions: which units? Before or after the trade? What if multiple orders hit the book at once? What if fund_units is temporarily stale?

How the same rule looks in Spec++.

In Spec++, you write the rule as an invariant on system state—a rule that must always hold. You say which state you care about and what must be true of it. 

invariant MaxOwnershipPerFund:
  for each fund, for each account:
    ownership_share(fund, account) <= 0.10

Plain English: For every fund and every account, the share of ownership cannot exceed 10%.

Around that invariant you define how actions may change state: booking trades, corporate actions, opening accounts. The toolchain proves that, under those rules, the invariant cannot be broken—or shows you the exact counterexample if it can.

Step 1
You write the specification.

Describe the domain: funds, accounts, holdings, trades. Add invariants in language a domain expert can read and a machine can check.

Step 2
The system proves properties about it.

The Spec++ toolchain checks legal sequences of actions. If the 10% rule could break, you get the failing sequence—not a production incident three weeks later.

Step 3
AI generates code that implements the spec.

Generation targets a specification that already passed checks. The code is an implementation of proven intent, not model improvisation.

Step 4
At runtime, the rules are enforced again (regulated deployments).

In production, the same invariants can be enforced in the Compliance Operator (CECO) validator, with cryptographic proof and a hash-chained audit log per decision—so “we deployed correctly once” is not the only line of defence.

Where Spec++ meets your IDE and CI.

Spec++ Pipeline (product—in active R&D) is how teams keep specifications as live as code when agents commit daily: natural language clauses in Git, lift to structured Spec++, provenance in pull request review, checks in GitHub Actions. Same methodology; tooling for Cursor and GitHub.

Discuss an SDD programme → Talk about a build engagement →

What this feels like as an engineer.

  • Your unit of work becomes a rule, not a ticket. “Implement Rule 17.3” means expressing it in the spec—not scattering if statements.
  • Debugging moves upstream. Tighten the specification and regenerate instead of chasing logs.
  • Conversations with product and compliance get crisper. Point to a named invariant: “Is this what you mean?”
  • Ownership is clearer. When a regulator asks why a decision was allowed, the answer is a named rule you authored.
  • A career path exists. Product, junior engineering, and QA can move into specification stewardship—operating the pipeline, guarding provenance—without everyone becoming a formal methods researcher.

If you want the underlying formalism or a comparison to TLA+, Dafny, or Alloy, see how Spec++ relates to existing work or the glossary for plain-language definitions.