Scope-Forge

Scope-Forge treats a policy as mathematics: every question about it is answered exactly, at build time, by a compiler whose own code is machine-checked with Verus. A proof covers every possible input, so the logic it covers has no untested case, which is exactly the case an attacker accelerated by AI searches for.

Why now. In 2026 Google's Threat Intelligence Group reported, for the first time, a threat actor using a zero-day exploit developed with AI, with "high confidence that the actor leveraged an AI model to support the discovery and weaponization of this vulnerability": a script that "enables the user to bypass two-factor authentication (2FA) on a popular open-source, web-based system administration tool" (Google Threat Intelligence Group, May 2026).

In November 2025 Anthropic reported a campaign in which "the threat actor was able to use AI to perform 80-90% of the campaign, with human intervention required only sporadically", at "an attack speed that would have been, for human hackers, simply impossible to match" (Anthropic, November 2025). In August 2026 the NSA, CISA, FBI, Department of Energy and EPA jointly advised that AI-generated exploitation scripts are "dramatically reducing the technical expertise and time required to develop working ICS exploitation scripts and malicious tools" (joint advisory, August 2026).

"31% of breaches now start with software vulnerabilities, beating stolen passwords as the top way attackers get in" (Verizon 2026 DBIR), and "the time between disclosure and exploitation has shrunk to days" (UK NCSC, May 2025). Testing checks the cases someone thought of; a proof has none.

If you run OPA or Cedar today: they evaluate each request against the policy you deployed, and Cedar's analysis can check a policy set when you run it. Scope-Forge makes the check the build: a contradiction does not compile, every security rule is held against every possible record, and the code that decides each request is itself machine-checked.

Go deeper: Type Algebra.

Write the policy, not the proof. Write "contractors can never hold a clearance that permits restricted reads" into the policy once, and no later change can break it without the build failing, showing your reason, and producing the exact record that would have slipped through.

Below, that sentence as an assertion.

Principal requires {
    employment: str where in "employee" || "contractor"
    clearance: str where in "none" || "confidential" || "secret"
}

Contractor requires Principal && {
    employment: str where == "contractor"
    clearance: str where == "none"
}

RestrictedRead requires Principal && {
    clearance: str where in "confidential" || "secret"
}

assert Contractor never in RestrictedRead
    because "contractors never hold a clearance that permits restricted reads"

Months later, an edit grants contractors a confidential clearance.

Contractor requires Principal && {
    employment: str where == "contractor"
    clearance: str where in "none" || "confidential"
}

  because "contractors never hold a clearance that permits restricted reads"
  counterexample, a record in both sets
    { employment: "contractor", clearance: "confidential" }

An assertion relates two sets: in (a subset), not in, never in (no record in both), equal and not equal.

The compiler says exactly why and where, with a suggested fix. Two rules whose requirements cannot both be met leave an empty set, and an empty set is a compile error.

Cleared requires {
    clearance: num where in 4..5
}

Probationary requires {
    clearance: num where in 1..2
}

ProbationaryRelease requires Cleared && Probationary

  Cleared.clearance
    admits 4..5
  Probationary.clearance
    admits 1..2
  the intersection is empty
  help: widen one range until 4..5 and 1..2 overlap, or do not compose them

Groups are described by what their members are and combined freely, so a person in several groups is natural. A role builds on any number of parent roles, and the whole hierarchy is checked at compile time.

DayShift requires {
    hour: num where in 6..18
    clearance: num where in 1..4
}

Mission requires {
    hour: num where in 10..22
    clearance: num where in 2..5
}

MissionDay requires DayShift && Mission

A rule can also relate one field to another field of the same record: the approver must not be the requester; the request time must be before the credential's expiry. The relation is a comparison (before, after, at most, at least, equal, not equal) against the other field's resolved value, across nested records. Below, the expiry rule.

PositiveTime: num where > 0

Request requires {
    expires: PositiveTime
    now: PositiveTime
}

Live requires Request && {
    now: PositiveTime where < resolved This.expires
}

Stale requires Request && {
    now: PositiveTime where >= resolved This.expires
}

assert Stale never in Live
    because "a request made at or after its credential's expiry is never live"

Go deeper: Numeric Sets for rules on numbers, and Regular Languages for rules on text.

An application of the approach, not a cross-domain product: the same set-based policies and compile-time checks apply to the policy layer of a cross-domain rule set, classification labels and the rules for moving data between security domains, as sets checked at build time.

Label requires {
    level: num where in 0..4
    marking: str where in "NOFORN" || "REL" ++ (" " ++ ("A".."Z")+)+
}

CrossDomainTransfer requires Label && {
    level: num where in 1..3
    marking: str where not in "NOFORN"
}