Language Reference

An .ag file is a sequence of top-level declarations. Order does not matter; the compiler resolves references during type checking.

Enforcement Semantics

aglang declarations have explicit enforcement levels:

Declaration	Level	Meaning
invariant deny flow	formal_z3	Extracted flow facts are checked against SMT-LIB constraints in Z3.
invariant deny reach	formal_z3	Transitive flow reachability is checked in Z3.
invariant deny dataflow	formal_z3	Dataflow facts inferred from handled data and extracted reachability are checked in Z3.
data_policy	formal_z3	Data classification and jurisdiction rules are checked against propagated data reachability.
trust_policy	formal_z3	Trust-boundary auth and classified data boundary rules are checked from extracted facts and declared node metadata.
change_policy	formal_z3	Touched-component facts are checked against SMT-LIB implication rules in Z3.
di_policy	formal_z3	Definite constructor-injection, lifetime, and service-locator facts are checked in Z3.
contract	deterministic_policy	Route facts are compared against declared implements/consumes contracts.
workflow_policy	deterministic_policy	GitHub Actions facts are checked for release, deploy, publish, permission, and step-order rules.
invariant require encryption	advisory	Reported as a warning because static extraction does not yet prove encryption.
machine	advisory	Emitted to agent context; transition extraction is not enforced yet.
permission	formal_z3	Authorization intent is emitted and can be enforced when extractors produce definite operation and role-check evidence.

formal_z3 and deterministic_policy violations block checks. advisory declarations guide agents and docs, but do not block by themselves unless a future extractor/gate promotes them.

Infrastructure Node

Declares an infrastructure or runtime entity that components run on or interact with.

node <name> : <node_type> {
  trust: trusted | untrusted | semi_trusted
  protocol: https | grpc | ws       // optional
  auth: none | jwt | oauth2 | api_key // optional
}

Example:

node api_runtime : server { trust: trusted protocol: https }
node ledger_db : postgres { trust: trusted auth: mtls }

Node types come from the stdlib, including server, ci_runner, package_registry, static_host, release_host, postgres, redis, s3_bucket, and agent_runtime.

Component

Declares a logical code component and maps it to source files.

component <Name> {
  runs_on: <node_name>
  paths: "<glob>"
  role: presentation | application | domain | data_access | infrastructure | integration | test // optional
  layer: <LayerName>        // optional
  implements: <ContractName> // optional, comma-separated
  consumes: <ContractName>   // optional, comma-separated
  handles: <DataType>        // optional, comma-separated
  repo: <RepoName>           // optional
}

Example:

component PublicApi {
  runs_on: api_runtime
  paths: "src/api/**/*.ts"
  implements: UsersApi
}

Resource

Declares an architectural capability that components may access, such as secure storage, local preferences, platform hardware, or external APIs.

resource <name> : <resource_type> {
  trust: trusted | untrusted | semi_trusted
  protocol: https | grpc | ws          // optional
  auth: none | jwt | oauth2 | api_key  // optional
}

Built-in resource types include secure_storage, local_preferences, external_api, local_database, reactive_stream, message_bus, file_system, sensor, and device_hardware.

Example:

resource SecureStorage : secure_storage { trust: trusted }
resource LocalPreferences : local_preferences { trust: semi_trusted }
resource ExternalNetwork : external_api { trust: untrusted protocol: https }

Invariant

Flow invariants declare component or node relationships that must not be violated.

invariant <Name> {
  deny flow <ComponentOrNode> -> <ComponentOrNode>
  deny reach <ComponentOrNode> -> <ComponentOrNode>
  deny flow role <RoleName> -> resource <ResourceNameOrType>
  deny flow layer <LayerName> -> resource <ResourceNameOrType>
  deny dataflow <DataType> -> <ComponentOrNode>
  require encryption on flow <ComponentOrNode> -> <ComponentOrNode>
}

Example:

invariant Layering {
  deny flow PublicApi -> ledger_db
  deny flow role presentation -> resource secure_storage
}

deny flow is direct-only for compatibility. Use deny reach to block transitive paths such as UI -> Service -> Db. require encryption on flow is currently advisory because extractors do not yet prove encrypted transport.

deny dataflow is also Z3-backed. It blocks when a component that handles a data type can reach the denied target through one or more extracted flows.

Data Metadata And Policies

Data declarations can carry classification and jurisdiction metadata:

data CustomerProfile {
  classification: pii
  jurisdiction: eu
  id: UUID
}

data_policy blocks use those labels over propagated data reachability:

data_policy Privacy {
  deny classification pii -> untrusted
  deny jurisdiction eu -> NonGdprService
}

The first rule blocks classified data reaching any declared entity whose trust metadata is untrusted. The second blocks data with a specific jurisdiction from reaching a named component, node, or resource.

Trust Policy

Trust policies use trust: and auth: metadata from nodes and resources. Components inherit metadata from their runs_on node.

trust_policy Boundaries {
  require auth untrusted -> trusted
  deny flow trusted -> untrusted when data pii
}

require auth blocks an extracted path from an untrusted entity to a trusted entity when the target has no declared auth. deny flow ... when data blocks classified data crossing the declared trust boundary.

Contract

Contracts define interface shapes between components.

contract UsersApi {
  GET  "/api/users"      -> User[]
  POST "/api/users"      -> User
  query viewer()         -> User
  rpc GetUser(UserId)    -> User
  publishes: "user.created"
  subscribes: "user.deleted"
}

Components opt into contract enforcement with implements: or consumes:.

Workflow Policy

workflow_policy blocks enforce GitHub Actions release and deployment safety. Workflow YAML files are modeled as components, and publish/deploy/release targets are modeled as CI/CD nodes.

node github_actions : ci_runner { trust: trusted }
node npm_registry : package_registry { trust: trusted auth: api_key }
node github_pages : static_host { trust: trusted auth: oauth2 }

component ReleaseWorkflow {
  runs_on: github_actions
  paths: ".github/workflows/release.yml"
}

workflow_policy ReleaseSafety {
  allow publish ReleaseWorkflow -> npm_registry when tag "v*.*.*"
  deny publish * -> npm_registry when pull_request
  require before ReleaseWorkflow "npm test" -> "npm publish"
  deny permission * contents: write when pull_request
}

Supported actions are publish, deploy, and release. Conditions support when tag "<glob>", when branch "<glob>", and when pull_request.

Change Policy

change_policy blocks enforce that related components are updated together in the same checked diff.

change_policy DocsFreshness {
  require touched CliReferenceDocs when touched CliCompiler
  require touched ReadmeDocs when touched CliCompiler
}

Semantics: if any staged file maps to the trigger component, at least one staged file must map to the required component. The gate emits Z3-backed change_violations[] when the implication cannot be satisfied.

Change policies prove that declared surfaces changed together; they do not prove that prose is semantically complete.

Dependency Injection Policy

di_policy blocks enforce dependency injection boundaries when the runtime can extract definite DI facts. The built-in C# extractor currently detects constructor injection, AddSingleton / AddScoped / AddTransient registrations, and IServiceProvider / GetRequiredService<T> service-locator usage.

component Views {
  runs_on: app_runtime
  paths: "src/**/Views/**/*.xaml.cs"
}

component ViewModels {
  runs_on: app_runtime
  paths: "src/**/ViewModels/**/*.cs"
}

component BleManager {
  runs_on: app_runtime
  paths: "src/**/Infrastructure/Bluetooth/**/*.cs"
}

component Repositories {
  runs_on: app_runtime
  paths: "src/**/Infrastructure/Persistence/**/*.cs"
}

component Application {
  runs_on: app_runtime
  paths: "src/**/Application/**/*.cs"
}

di_policy DependencyInjection {
  deny inject Views -> BleManager
  deny inject_reach Views -> Repositories
  deny inject ViewModels -> Repositories
  deny lifetime singleton -> scoped
  deny lifetime_reach singleton -> scoped
  deny resolve IServiceProvider from Application
}

Semantics:

• deny inject A -> B blocks a constructor dependency from component A to component B.
• deny inject_reach A -> B blocks a transitive constructor dependency path from component A to component B.
• deny lifetime singleton -> scoped blocks a singleton-registered service depending on a scoped-registered service.
• deny lifetime_reach singleton -> scoped blocks a transitive lifetime path from singleton to scoped.
• deny resolve IServiceProvider from Application blocks service-locator access from Application.

Each blocking DI fact becomes an SMT assertion such as (assert (Injects Views BleManager)), (assert (InjectReach Views Repositories)), or (assert (LifetimeReach Lifetime__singleton Lifetime__scoped)). The compiled di_policy contributes the opposite implication, so Z3 returns UNSAT and the JSON verdict reports a di_violation.

State Machine

State machines describe allowed transitions for a data type field. They are advisory in the current runtime.

enum OrderStatus { Draft | Active | Archived }

data Order {
  status: OrderStatus
}

machine OrderLifecycle on Order.status {
  allow transition Draft -> Active
  deny transition Active -> Draft
}

Permission

Permissions describe role/action rules. They are formal when extractors provide definite authorization evidence; otherwise they remain agent-visible intent.

enum Role { Admin | Member }

permission ProjectAccess on Project {
  allow Role.Admin -> *
  deny Role.Member -> delete
}

Data And Enum

data User {
  classification: pii
  jurisdiction: eu
  id: UUID
  email: String
  roles: List<Role>
}

enum Role { Admin | Member }

Import

Import another .ag file to compose large specs:

import "./shared/base.ag"
import "./services/auth.ag"

Cyclic imports are detected and rejected at compile time.

Comments

// Single-line comment