Proofs, Not Reviews

The Precedent

Tao's Answer for Math

In mathematics, peer review was the trust mechanism for centuries. Terence Tao replaced it with formal verification using Lean — proofs that machines check mechanically.

What peer review achieves

Correctness guarantee
Error catching
Reproducibility
Building on prior work
Scalable trust

How Lean achieves the same

Mechanical proof checking — every step verified
Static checking across all cases
Deterministic compilation
Composable proven theorems
Trust is mathematical, not social — unlimited contributors

✓ The equational theories project verified 99.9963% of 22 million implications in 19 days

Our Answer for Software

The Bottleneck-by-Bottleneck Solution

For each bottleneck in modern software development, here is what "proof" means concretely.

Security — Prove, Don't Audit

Formal taint analysis across all code paths, not just tested ones

PROVE User input never reaches SQL query without sanitization — across ALL code paths, not just tested ones

PROVE Every public endpoint requires authentication

PROVE No known-vulnerable library functions are reachable from production code paths

"Security audit checks what you remembered to test. Formal verification checks everything."

Architecture — Prove, Don't Convention

Enforced module boundaries, not just agreed-upon conventions

PROVE External API calls only happen via the integration layer

PROVE Module X has no dependency on module Y (architectural boundary)

PROVE Data access layer is the only code that touches the database

"Architecture conventions break silently. Proven constraints break loudly — at definition time."

Properties — Prove, Don't Assume

Verified semantic properties on every function, not hopeful assumptions

PROVE This function is idempotent (calling it twice = calling it once)

PROVE This function is pure (no side effects, deterministic)

PROVE This operation is commutative (order doesn't matter)

PROVE This module is fully encapsulated (no leaking internal state)

PROVE This data transformation is monotonic (adding input never removes output)

Higher Abstraction — Prove Your Architecture Diagrams

Architecture diagrams where every arrow IS a verified condition

PROVE Generate C4 diagrams, event-storming flows, architecture diagrams from verified properties

PROVE Each arrow at the visual layer IS a verified condition — not just a drawing

"Your architecture diagram isn't just a drawing — it's a proof."

Under the Hood

How: Attribute Grammars + Abstract Interpretation

You know how a spreadsheet computes formulas automatically? This framework does the same with code properties. You declare what each piece of code should guarantee, and the framework verifies it — for ALL possible inputs, not just test cases.

Properties flow in two directions through your code tree:

TypeScript-like syntax for declaring properties and writing equations:

// Declare properties
declareAttr('isPure', { direction: 'syn', on: ['Function'] })
declareAttr('authRequired', { direction: 'inh', on: ['Endpoint'] })

// Write equations
equations({
  ArrowFunction: {
    syn: {
      isPure: and(noSideEffects(body), allChildrenPure(params))
    }
  },
  APIRoute: {
    childInh: {
      handler: {
        authRequired: literal(true)
      }
    }
  }
})
      

Traditional Static Analysis

TypeScript's type system is bottom-up only: infers types from values upward. Can't express "this endpoint MUST have auth" — only "this function returns string."

AG Approach — Both Directions

Bottom-up: infer properties from code structure.
Top-down: impose constraints from architecture onto implementation.

"It's like TypeScript's type inference, but for ANY property, in BOTH directions."

Abstract Interpretation

Instead of running code with concrete values (x = 42), we represent all possible values symbolically (x: integer, positive). This means we prove properties over all inputs, not just test samples.

The Sudoku Effect

The more information modeled, the more that can be inferred. Each proven property constrains the space of possibilities and enables proving additional properties — like filling in a sudoku where each answer reveals new ones.

Two Evaluation Pipelines

LAZY (Dev)

decorate(tree, compiled)
Attributes computed on demand. Ideal for interactive dev tools.

COMPILED (Prod)

compileEvaluator(ag)
Single generated JS function. 10-100x faster. Eager evaluation.

Self-Hosted

The validator that checks AG specifications is itself an AG. The framework validates itself — a concrete demonstration of its expressiveness.

The Key Unlock

The Agent Feedback Loop

The framework doesn't just verify — it creates a closed loop where AI agents improve code until properties are proven.

Example 1: Proving Purity

// Agent tries to prove this function is pure import { logToFile } from './logger'; function calculateTotal(items: Item[]): number { logToFile('Calculating total...'); return items.reduce( (sum, i) => sum + i.price, 0 ); }

✗

isPure: FAILED
imports side-effectful module 'logger'

⋯

testable: pending

⋯

convertible to Rust: pending

Agent detects: function imports side-effectful logToFile module directly.

Example 2: Immutability Cascade

// Agent tries to prove variable is immutable let config = loadConfig(); function processItems(items: Item[]) { for (let i = 0; i < items.length; i++) { transform(items[i], config); } }

✗

isImmutable(config): FAILED
uses 'let' instead of 'const'

⋯

loop deterministic: pending

⋯

processItems pure: pending

Agent detects: config uses let — could be reassigned.

Example 3: Auth Enforcement

// Agent declares: all endpoints require auth app.get('/api/users', authMiddleware, getUsers); app.post('/api/orders', authMiddleware, createOrder); app.get('/api/health', healthCheck); app.put('/api/profile', authMiddleware, updateProfile);

✓

/api/users — auth: PASS

✓

/api/orders — auth: PASS

✗

/api/health — auth: MISSING

✓

/api/profile — auth: PASS

Framework checks ALL paths: /api/health has no auth middleware.

Each fix doesn't just solve one problem — it makes the ENTIRE codebase more provable. Like filling in a sudoku: each answer eliminates possibilities and reveals new ones. A single let→const can cascade into proving the loop deterministic, the function pure, and the module side-effect-free.

The Paradigm Shift

What This Replaces

Every row is a process that used to require human judgment. Now it's mechanical.

Before (Review-Based)	After (Proof-Based)
Security audit Human reviews code paths manually	Security proof Framework checks ALL paths formally
Architecture review Senior engineer spot-checks boundaries	Architecture proof Boundaries enforced continuously
Code review Reviewer trusts or re-reads manually	Property proof Machine verifies claims mechanically
Testing Check specific inputs and edge cases	Formal analysis Verify over ALL possible inputs
Convention "We agreed to do X"	Proven constraint "The system won't allow not-X"
Documentation "This endpoint requires auth"	Verified property Proven that no unauthenticated path exists