Spec++ · The method

How a policy is written so the gate can check it.

Spec++ is the way a policy is written so the Compliance Operator can check it and enforce it. It is ready to use in a customer engagement. The engagement is Lean-proved high-assurance software, or the policy inside that work. Specification-driven development is how we do that work with your engineers.

This page is for an engineer who is already in the conversation. It is not the thing a buyer came to purchase. The mathematical terms stay on the glossary.

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 implements that specification. It is not the model improvising.

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 the method meets the engagement.

Spec++ stays the method. In a software engagement, your engineers and ours keep the policy in the same place as the code: versioned, reviewed, and checked before it is enforced.

Talk about a software 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 someone asks why a decision was allowed, you can point to the named rule.
  • A career path exists. Product, junior engineering, and QA can learn to keep the specification, without everyone becoming a formal-methods researcher.

The terms are on the glossary.