PROBABLE TO PROVABLE

From Probable to Provable

The framework for AI-assisted development that actually works.

Inspired by Bertrand Meyer's work on Design by Contract and software verification.

The Core Insight

AI produces statistically likely code. Not proven correct code. Likely code.

"Likely" works for one module. "Likely" fails at scale.

The Math

If each module is 99.9% correct:

100 modules

0.999^100 = 90.5%

500 modules

0.999^500 = 60.6%

1,000 modules

0.999^1000 = 36.8%

5,000 modules

0.999^5000 = 0.7%

Real systems have thousands of modules. "Probably correct" becomes "probably broken."

The Solution

Combine AI generation with formal verification.

AI Generates

Fast, bulk, pattern-matching

Contracts Verify

Complete, automatic, every execution

Probable + Verification = Provable

The Process

SPECIFICATION

Write contracts BEFORE implementation. Define what must be true.

GENERATION

AI generates implementation to satisfy contracts. Fast, bulk, pattern-based.

VERIFICATION

Compiler checks types. Runtime checks contracts. Tests check scenarios.

ITERATION

Contract violation? Fix spec or implementation. Repeat until correct.

The "True But Incomplete" Trap

AI often generates contracts that are true but miss guarantees. Step through this example:

AI might write:

add_item (a_item: ITEM)
    do
        items.extend (a_item)
    ensure
        has_item: items.has (a_item)
    end

✓ True... but what about count?

Complete contract:

add_item (a_item: ITEM)
    do
        items.extend (a_item)
    ensure
        has_item: items.has (a_item)
        count_increased: items.count = old items.count + 1
        only_one_added: items.occurrences (a_item) = old items.occurrences (a_item) + 1
    end

✓ Complete: item added, count grew, exactly one copy added

⚠ The incomplete contract misses bugs:

• AI accidentally adds item twice → has_item still passes!

• AI forgets to actually add → only caught if has_item checked

• Complete contract catches BOTH immediately

Click Step to see the difference

AI writes a postcondition: "the item is in the list"

This is TRUE... but is it COMPLETE?

Complete contract also verifies the same thing...

PLUS: the count increased by exactly 1

PLUS: only ONE copy was added (not duplicates)

The incomplete contract misses real bugs!

Always ask: "What ELSE is guaranteed?"

The Implication

AI without verification: Faster bugs at scale.

AI with verification: Faster correctness at scale.

The technology for verification exists. It's called Design by Contract. It's built into Eiffel.

How DBC Works Get Started