Real incidents. Real cost. Each one preventable with a single proven property.
Every one of these failures was detectable before deployment. The property that would have caught it? A single declarative rule.
User-controlled strings reached JNDI lookup in Log4j, enabling remote code execution on millions of servers worldwide.
"No user-controlled input reaches privileged system calls without sanitization"
Taint safety: user-controlled data (HTTP headers, query params, form fields) must never flow to sensitive sinks (JNDI lookup, command execution, SQL queries) without passing through a sanitization function. This is a data-flow property that must hold across ALL code paths.
Declare user input as "tainted" source. Declare JNDI lookup as "sensitive sink." Prove: no path from tainted source to sensitive sink exists without sanitization. The AG framework traces this as inherited/synthesized attributes across the entire AST — covering ALL code paths, not just tested ones. A single taint-analysis property, checked at build time, would have flagged every vulnerable call site.
Malicious code injected into the build pipeline was distributed via legitimate software updates, compromising US government agencies and Fortune 500 companies.
"Build output is a pure function of checked-in source code"
Build hermeticity: the compiled output must depend ONLY on tracked, versioned inputs. Any undeclared dependency, runtime injection, or build-time code modification violates this property. The Sunburst attack modified the build process itself, injecting backdoor code that never existed in the source repository.
Prove build pipeline hermeticity — that the compiled output depends ONLY on declared inputs. Model the build graph as a tree: source files as leaves, build steps as interior nodes. Declare a "provenance" attribute that flows up. Prove: every node in the output tree traces back to a checked-in source. Any undeclared dependency or runtime injection fails verification automatically.
A public-facing web application endpoint lacked authentication, allowing direct access to internal databases containing 147 million personal records. Settlement exceeded $700M.
"All public endpoints enforce authentication before accessing user data"
Authentication enforcement: every public endpoint that accesses user data must have an authentication middleware in the request path. This is an inherited attribute — the "is-authenticated" property must flow from the route definition down to every data-access node.
Declare authentication as an inherited attribute flowing from route definitions. Prove: no data-access node is reachable from a public endpoint without auth middleware in the path. The framework checks this for ALL endpoints — not just the ones you remember to test. One missing auth guard on one forgotten endpoint caused a $700M+ breach. Formal verification checks every single path.
A faulty sensor configuration update caused a null pointer dereference in a kernel-mode driver, bricking 8.5 million Windows devices and disrupting global airlines and banking.
"Driver update cannot cause kernel panic / system halt"
Totality + null safety: all code paths in the driver handler must terminate without panic for all possible configuration inputs. No pointer dereference may occur without a null check on the path. The CrowdStrike driver read a field from a configuration blob without validating it wasn't null — for a single configuration variant.
Prove that all code paths in the update handler are total (terminate without panic) for all possible configuration inputs. Prove null safety — no pointer dereference without a null check on the path. This is exactly what Rust's type system enforces via Option<T>. The AG framework generalizes this: declare "nullable" as an attribute, prove every dereference has a check.
A missing bounds check in OpenSSL's heartbeat extension allowed attackers to read arbitrary server memory, exposing private keys and credentials from an estimated 66% of web servers.
"All memory access is within declared bounds"
Bounds safety: every array/buffer access index must be provably within the allocated range. The heartbeat handler copied payload_length bytes from the request without checking that the actual payload was that long — a single missing if statement that exposed the internet.
Prove bounds safety — that every array/buffer access index is provably within the allocated range. This is exactly what Rust's borrow checker does at compile time for Rust code. The AG framework generalizes this to arbitrary properties in any language: declare "buffer-size" and "access-index" as attributes, prove access-index < buffer-size at every access point.
A race condition in a concurrent state machine allowed a radiation therapy machine to fire a full-power beam with incorrect positioning, causing 6 patients to receive massive radiation overdoses.
"Concurrent state transitions cannot produce unsafe configurations"
State safety: no reachable combination of concurrent states may violate a safety invariant. The Therac-25 had a race condition where the operator could change the beam type while the machine was still configuring, resulting in full-power radiation without the correct shielding.
Model the state machine as a tree. Declare safety invariants as attributes. Prove: no reachable state combination violates the safety property. Formal verification of state machines is one of the oldest and most proven applications of the technique — it's how hardware vendors have verified chip designs since the 1990s. The same mathematics applies to software.
Auth required. Bounds checked. Input sanitized. Build is hermetic.
Convention, code review, testing, "best practices," manual checklists.
One endpoint, one code path, one config variant — missed by all of the above.
Billions in damage. Millions of users affected. Lives lost.
Testing checks specific inputs. Code review checks what the reviewer remembers to look for. Formal verification checks ALL possible cases. The incidents above were all detectable — if anyone had been checking comprehensively.
Each property is a single declarative rule. Each prevents an entire class of failures.
Prove no user-controlled input reaches sensitive sinks without sanitization.
Prevents: Log4Shell, SQL injection, XSS
Prove all public endpoints enforce auth before accessing user data.
Prevents: Equifax-class data breaches
Prove known-vulnerable functions are not reachable from production code paths.
Prevents: exploitation of unpatched dependencies
Prove every external input is validated before processing.
Prevents: injection, buffer overflow, DoS
Prove no code path transitions from low to high privilege without explicit authorization.
Prevents: unauthorized access escalation
Prove no cross-boundary imports exist — internal modules stay internal.
Prevents: architecture erosion, coupling debt
Prove the dependency graph is acyclic and respects declared layer ordering.
Prevents: circular dependencies, layer violations
Prove external calls only happen through designated integration layers.
Prevents: SolarWinds-class supply chain attacks
Prove database access only happens through the designated data layer.
Prevents: unaudited data access, schema drift
Prove calling a function twice produces the same result as calling it once.
Prevents: duplicate charges, double submissions
Prove a function has no observable side effects beyond its return value.
Prevents: hidden state mutations, test flakiness
Prove a function terminates and returns a value for all possible inputs.
Prevents: CrowdStrike-class crashes, null panics
Prove no pointer or reference dereference occurs without a prior null check.
Prevents: Heartbleed-class memory corruption
Prove order independence — processing items in any order yields the same result.
Prevents: race conditions, ordering bugs
Prove adding input never removes output — the function only grows.
Prevents: data loss, vanishing results
Prove PII never reaches logs, analytics, or third-party services without consent.
Prevents: GDPR violations, accidental data leaks
Prove all state mutations are logged to the audit system.
Prevents: compliance audit failures, SOX violations
Prove exactly which code paths handle regulated data — no more, no less.
Prevents: scope creep, unknown regulatory exposure
Prove data doesn't leave designated geographic regions or environments.
Prevents: sovereignty violations, cross-border leaks
Individual proofs at the function level build into system-level guarantees. Each layer inherits the certainty of the layer below.
Your architecture diagram isn't just documentation — it's a proof. Each arrow is a verified property. Each box is a composition of proven guarantees. When something changes, the proofs re-evaluate automatically.
The cost of NOT proving far exceeds the cost of proving
Preventable with one taint analysis property
Preventable with one auth enforcement property
Preventable with one null safety property
Preventable with one state safety property