How to verify Termin's security claims

Security claims only matter if they can be verified. Termin's structural claims rest on five interlocking layers of defense-in-depth, each of which can be checked independently. This page describes the layers, how a reader can verify each one, and what is not yet proven.

The comparison many evaluators reach for is Rust. Rust can claim thread safety because it is a functional language with a formal ownership type system, and functional languages with ownership types cannot produce a data race — that is solid syllogistic reasoning backed by decades of formal work. Termin does not have a formal proof. What Termin has is a sequence of five independently verifiable layers, each of which closes a specific class of failure, and a behavioral conformance suite that exercises all five. The defense is cumulative. Each layer is weaker than a proof; the combination is meaningful.

The rest of this page describes the layers, how to verify each one, and what remains to be done.

# The even-if chain

The short form of the argument. If you only read one thing on this page, read this.

1. You cannot express something unsafe in the language. The grammar rejects it.
2. Even if you did (ungrammatical Termin), the compiler would catch it and return an error. The analyzer rejects it.
3. Even if it didn't (malicious IR that bypasses the compiler), the runtime enforces the security invariants and rejects malformed IR. The runtime's structural checks fire at load time.
4. Even if it didn't (bug or flaw in the runtime), the conformance test suite would alert you to the non-conforming behavior. The suite runs against every conforming runtime.
5. Even if it didn't (gap in behavioral testing), third-party audit and red-teaming would identify findings, which feed back into hardening the language, runtime, and conformance suite. This layer is a v1.0.0 goal, not a current reality.

Each step independently blocks a specific class of failure. An attacker — or a well-meaning agent generating Termin specifications — would have to defeat all five to introduce a structural vulnerability. The layers are not rhetoric. They are four working mechanisms plus one honest commitment.

# The five layers

# Layer 1 — Declarative grammar, non-Turing-completeness

The Termin DSL is declarative. You describe what the application does, not how to do it. The grammar does not provide constructs for:

• Assembling SQL queries from strings
• Concatenating user input into executable commands
• Producing template output that escapes the boundary
• Spawning subprocesses, opening arbitrary files, making arbitrary network calls
• Modifying access-control state at runtime
• Mutating schemas without going through the compiler

Certain violations are not just rejected — they are inexpressible. There is no syntax for "SQL string plus user input." The language provides parameterized access and identity-scoped operations; it does not provide the machinery to produce injectable constructs. This is the strongest layer because it rules out entire classes of failure at the lexical level.

How to verify: Read the grammar. It is a PEG grammar (Parsing Expression Grammar). Walk through the production rules and observe that there is no rule for string concatenation into queries, no rule for shell execution, no rule for raw template output. The absence is the evidence.

# Layer 2 — Compiler invariant enforcement

Even a well-formed specification can be semantically wrong. The compiler's analyzer enforces a set of invariants that the grammar alone cannot express:

• Every access rule references a declared scope.
• Every state transition has a source state that exists, a destination state that exists, and a scope that exists.
• Every content reference resolves to a declared content type.
• Every boundary contains its declared content and computes.
• Every Compute that modifies confidentiality-protected data declares its reclassification.
• Every role-story references a declared role; every page references declared content.
• Every action button on a table has a matching access rule on the content.

The analyzer emits structured error codes (TERMIN-S020, TERMIN-S021, TERMIN-S030, …) with fuzzy-match suggestions, so authors see what went wrong and how to fix it.

How to verify: Read the analyzer source. Every SemanticError has a code and a message. Read the analyzer tests — the test suite covers each invariant with both a passing case and at least one failing case. Run the tests yourself (python -m pytest tests/test_analyzer.py); they pass against the public reference implementation.

# Layer 3 — Runtime behavioral contract

The runtime reads the compiler's intermediate representation (IR) and serves the application. A conforming runtime is bound by a behavioral contract specified alongside the IR JSON Schema. The contract covers:

• Identity resolution and scope evaluation on every request.
• Access-control checks at every route, every state transition, every Compute invocation, every Channel send, every page render.
• State-transition enforcement — only declared transitions permitted, only from the declared source state, only with the declared scope.
• Boundary crossing restricted to declared Channels.
• Confidentiality redaction before data leaves the Boundary, with taint propagation on computed values.
• Audit log completeness for every Content modification and state transition.

The runtime rejects IR that violates the schema. The runtime rejects callers whose identity does not carry the required scope. The runtime rejects transitions that are not declared. These behaviors are the contract, not an implementation choice — every conforming runtime enforces them.

How to verify: Read the Runtime Implementer's Guide. Clone the reference runtime and read termin_runtime/. Every guarantee on the guarantees page links to the specific enforcement point in the runtime plus the conformance test that validates it.

# Layer 4 — Behavioral conformance suite

The conformance suite contains over 700 behavioral tests. The suite is runtime-agnostic: it takes any conforming runtime, drives it through a battery of positive and negative cases, and asserts that every structural guarantee holds. Examples of what the suite covers:

• Access control. Every CRUD verb is tested with both an in-scope caller (success expected) and an out-of-scope caller (403 expected). Role-appropriate and role-inappropriate cases are parametrized across every content type.
• State transitions. Every declared transition is attempted from every declared source state, with and without the required scope, from and to states that are and are not declared.
• Confidentiality. Records containing confidential fields are fetched by in-scope and out-of-scope callers; the suite asserts that out-of-scope callers see [REDACTED] markers and not the values.
• Data isolation. Cross-boundary reads and writes are attempted through every path the runtime exposes; the suite asserts that only declared Channels succeed.
• Injection resistance. Field values containing SQL-injection shaped strings, command-injection shaped strings, and CEL-expression-injection shaped strings are submitted through every ingress path; the suite asserts they are stored and returned as literal data, never interpreted.
• Malformed IR. The suite loads IR with missing required fields, wrong types, cycles, and unreachable states, and asserts the runtime rejects each case.

The suite exists so that a second or third conforming runtime — written in Rust, Go, TypeScript, or any other language — can be validated against the same behavioral contract. Pass the suite and your runtime inherits the Tier 1 structural guarantees.

How to verify: Clone the conformance suite. Read the tests — they are the plain-language version of the behavioral contract. Run them (python -m pytest tests/). They pass against the reference runtime. Read the suite's README to see how to point them at a different runtime.

The reference compiler has over 1,400 additional tests (compiler tests) covering the parser, analyzer, lowering, IR schema, and the reference runtime itself. These supplement the behavioral suite with white-box coverage of the compile pipeline.

# Layer 5 — Third-party audit

Before v1.0.0, the compiler, runtime, and conformance suite will be audited by software security professionals and hardened based on their findings. Options being explored include sponsored audits from security firms with open-source practices, community-funded audits, and pro-bono reviews through professional networks. The audit is on the roadmap.

Today, this layer is a commitment. If you need Layer 5 before deploying, wait for v1.0.0.

How to verify: Watch the roadmap. When an audit is scheduled, it will be listed there. When one completes, the findings will be published. No claim on this site asserts a completed audit that has not happened.

# An analogy: industrial robot safety

The technical description above is precise but abstract. An analogy that many readers find useful: how do we know that an industrial robot — humanoid or otherwise — is safe to operate around humans?

• Layer 1. The robot only understands commands that aim in a safe direction. There is no way to intentionally or accidentally get the robot to shoot you in the foot, because its command parser has no notion of "point gun at own foot."
• Layer 2. Even if someone issued an unsafe command, the robot's command parser would reject it. A malformed command does not silently execute in a degraded mode; it is refused.
• Layer 3. All robot installations are bound by hard environmental contracts — a safety cage, floor sensors, an emergency stop — that make it impossible for the robot to accidentally harm a person or itself. Even if you put your foot in harm's way, the robot only takes action when it is safe to do so.
• Layer 4. Every robot and its environment are tested against an exhaustive checklist of safety properties, including adversarial scenarios where a person behaves erratically or maliciously. The checklist is run before operation and periodically thereafter.
• Layer 5. Every installation is inspected by a third-party professional safety inspector before it is allowed to operate. This is a v1.0.0 goal for the Termin reference runtime.

The first four layers are working mechanisms. The fifth is a commitment. The combination is what lets a factory floor manager allow robots and humans to share a workspace.

# The honest Rust comparison

Rust can claim thread safety on the basis of a formal ownership type system and decades of applied academic work. A Rust program that compiles cannot produce a data race. That is a strong claim backed by mathematical proof.

Termin does not have that. Termin has an interlocking set of structural layers plus a behavioral conformance suite. Each layer is independently weaker than a formal proof. The combination is meaningful but not equivalent.

If you need the strength of a formal proof for your use case, Termin is not there yet and may never be there. Most enterprise evaluators find defense-in-depth plus behavioral verification sufficient for the properties Termin claims to enforce. Some do not. We are honest about which one you are.

# Write your own runtime

A practical observation: the conformance suite is what makes cross-runtime verification possible. It defines the behavioral contract without reference to the reference implementation's code. If you want Rust-level assurance, you can write a conforming runtime in Rust, validate it against the suite, and benefit from the declarative grammar's Layer 1 protection plus Rust's memory-safety guarantees on the runtime itself. The suite and the IR schema are the things you would write against; the reference runtime is only one implementation.

This is the ecosystem design: the Termin specification is the contract. The reference runtime is the first conforming implementation. Other conforming runtimes in other languages with other trade-offs are anticipated, welcomed, and expected.

# What this page does not claim

• Termin has not completed a third-party security audit. Layer 5 is a v1.0.0 commitment.
• Termin does not have a formal proof of correctness. Layer 1 rules out a class of failures at the grammar level, not with a mathematical proof.
• Termin does not prevent errors in business logic. Incorrect scope assignments, flawed state machine designs, and incorrect confidentiality declarations are the application author's responsibility; the runtime enforces that declarations are followed, not that they are appropriate for your organization.
• Tier 2 providers (vetted Compute, Channel, and Presentation providers) inherit Tier 1 at their boundary only after passing the conformance suite and a documented security review. The vetting process itself is still undesigned and is not in place today.

# Where to go next

• Guarantees — the structural properties this verification scheme is verifying, each linked to the specific conformance test that backs it.
• Why Termin — the founding thesis about audit surface reduction, which depends on these verifiable layers to be meaningful.
• Roadmap — the schedule for the Layer 5 third-party audit.
• Conformance suite — the tests. Clone, read, run.