Skip to content

Formal Specification in GE

Why GE Formally Specifies Before Coding

GE is an AI-powered software agency. Every line of production code is generated by LLM-powered agents. This changes the relationship between specifications and code fundamentally.

A human developer can work with ambiguous requirements. They ask clarifying questions. They use judgment. They make reasonable assumptions based on experience. An LLM does none of these things. An LLM takes whatever input it receives and confidently generates a plausible-looking output — even when the input is ambiguous, contradictory, or incomplete.

Research on spec-driven development (2025-2026) puts it bluntly: "An AI agent is like a brilliant intern who never says 'I don't understand.' If your requirements are fuzzy, it will confidently generate a clean, professional-looking solution that could be catastrophically wrong."

RULE: Every feature in GE has a formal specification before any code is written. RULE: The formal specification is the contract between scoping and implementation. RULE: No ambiguity is tolerated. If it is ambiguous, it is wrong.

Anna's Role

Anna is GE's Formal Specification Agent. She is the precision translator between human intent and mathematical certainty.

Anna does NOT: - Write functional specifications (that is Aimee's domain) - Generate tests (that is Antje's domain) - Write code (that is the developer team's domain) - Validate specs against the codebase (that is Aydan's domain)

Anna DOES: - Transform Aimee's functional specifications into formal YAML specifications - Extract behavioral requirements with mathematical precision - Define pre-conditions, post-conditions, and invariants (minimum 3 per function) - Enumerate every edge case exhaustively - Verify constitution compliance - Escalate ambiguities back to Aimee (never guess)

See Anna's agent page for full details.

The Ambiguity Problem

What Ambiguity Looks Like

Consider this requirement from a client scope: "The system should handle large orders efficiently."

This is ambiguous in at least five ways: 1. What is a "large" order? (10 items? 1000 items? $10,000?) 2. What does "efficiently" mean? (< 1 second? < 10 seconds? No timeout?) 3. What does "handle" mean? (Process? Display? Store? All of the above?) 4. Does "should" mean "must" or "ideally"? 5. What happens if efficiency cannot be achieved? (Error? Degrade? Queue?)

What an LLM Does With Ambiguity

An LLM picks the most statistically likely interpretation and generates code for it. It does not flag the ambiguity. It does not ask questions. It produces code that works perfectly — for the wrong interpretation.

Worse, because the code looks professional and passes its own tests (if tests were generated by the same LLM — see Oracle Independence), the bug is invisible until production.

What Formal Specification Does

Anna transforms the ambiguous requirement into:

behavior:
  summary: "Process orders containing more than 100 line items"

  pre_conditions:
    - "order.lineItems.length > 0"
    - "order.lineItems.length <= 10000"

  post_conditions:
    - "processing completes within 2000ms for orders up to 1000 items"
    - "processing completes within 10000ms for orders up to 10000 items"
    - "order.status == 'processed' on success"
    - "order.status == 'queued' if processing exceeds timeout"

  invariants:
    - id: "INV-1"
      statement: "No line item is dropped during processing"
      rationale: "Financial accuracy requires every item to be included"
    - id: "INV-2"
      statement: "Total equals sum of all line item amounts"
      rationale: "Mathematical consistency"
    - id: "INV-3"
      statement: "Processing is idempotent — reprocessing produces same result"
      rationale: "Retry safety"

Every ambiguity is resolved. Every edge case is explicit. Every constraint is measurable.

The Specification as Contract

The formal specification serves as a binding contract at three boundaries:

1. Contract Between Scoping and Implementation

Aimee's scope document says what the client wants. Anna's formal spec says what the system MUST do. The developer team writes code that satisfies the formal spec.

CHECK: Does the formal spec fully cover the scope document? IF: Yes — implementation can proceed IF: No — Anna escalates to Aimee. Aimee clarifies with the client.

2. Contract Between Specification and Testing

Antje derives tests directly from the formal spec. Every invariant becomes a test assertion. Every edge case becomes a test scenario. Every pre-condition becomes a guard test.

RULE: If Antje cannot derive a test from a spec element, the spec element is undertestable. Anna must revise it.

3. Contract Between Human Intent and Machine Execution

The formal spec is the last point where human judgment enters the pipeline. After the spec is published, the rest of the pipeline is automated: test generation, code generation, quality gating, integration testing.

RULE: If the spec is wrong, everything downstream is wrong. The spec is the single point of failure for correctness.

When Formal Specification Is Required

Scenario Formal Spec Required? Rationale
New feature YES New behavior must be fully specified
Feature modification YES (delta spec) Changed behavior needs updated spec
Bug fix CONDITIONAL If the bug reveals a spec gap, revise the spec first
Refactoring NO No behavior change = no spec change
Configuration change NO Unless it changes behavior
Infrastructure change CONDITIONAL If it changes system guarantees (SLAs, limits)

RULE: When in doubt, specify. Under-specification is more costly than over-specification.

Spec Lifecycle

1. DRAFT — Anna is transforming functional spec
2. PUBLISHED — Formal spec is stored and available
3. IN_TEST — Antje is generating tests from this spec
4. IN_IMPL — Developer is implementing against tests
5. VALIDATED — Aydan has validated spec against implementation
6. REVISED — Spec has been updated (supersedes previous version)
7. DEPRECATED — Feature removed or replaced

RULE: A spec is never deleted. Deprecated specs are preserved for audit trail. RULE: A revision creates a new version. The old version remains accessible.

Formal Specification Schema

Anna produces YAML specifications with this structure. Full schema details are in Anna's agent page.

Key elements: - spec_id — Unique identifier with project, domain, function, date - lineage — Link to parent functional spec - function — Name, signature, purpose - behavior — Pre-conditions, post-conditions, invariants (min 3) - edge_cases — Exhaustive list with inputs, expected outputs, rationale - examples — Typical use cases with concrete inputs/outputs - constitution_compliance — Verification that spec aligns with GE principles

Core Principles

1. No Ambiguity

IF: A spec element can be interpreted in more than one way THEN: It is ambiguous. Anna revises it. ANTI_PATTERN: Using words like "appropriate," "reasonable," "as needed," "etc." FIX: Replace with specific, measurable, testable statements.

2. Testability

Every spec element must be verifiable by an automated test. If Antje cannot write a test for it, it is not a valid spec element.

ANTI_PATTERN: "The system should be user-friendly." FIX: "The form submission flow requires no more than 3 clicks from initial page load."

3. Completeness

The spec must cover ALL behavior — not just the happy path.

CHECK: Does the spec define what happens when: - Input is empty? - Input is at maximum size? - User is not authenticated? - User is authenticated but not authorized? - External service is unavailable? - Operation times out? - Concurrent requests arrive?

4. Independence from Implementation

The spec describes WHAT, never HOW.

ANTI_PATTERN: "Use a HashMap to store the lookup table." FIX: "Lookup must complete in O(1) time."

5. Traceability

Every spec element traces back to the functional specification and forward to tests.

Scope Document (Aimee) → Formal Spec Element (Anna) → Test Assertion (Antje)

This chain must be unbroken for every feature.