Sensor family 01
Structural
“Is this artifact internally coherent?”
What belongs here
A sensor belongs here if it can reach its verdict by reading the artifact — its source, its types, its schema, its bill of materials — without running it against real inputs. The oracle is the artifact's own internal consistency: the code either type-checks or it does not, and the implementation cannot argue with the answer.
Contested placements
Build Provenance & SBOM is about where an artifact came from rather than whether its text is coherent; it sits here because it is a claim you can check without executing anything. Model Checking and Theorem Proving establish facts about behaviour, not structure, and are grouped here because they establish them before the system runs.
Where its signals arrive
- Compilation — Build stage. Is it a valid inhabitant of the language?
- Static analysis / types — Build stage. Is it internally coherent and structurally valid?
The atlas places every family on the same lifecycle grid; the framework defines the six dimensions each entry below is characterized along.
Entries (9)
Build Provenance & SBOM
Is the artifact you are about to deploy structurally the one your pipeline built? A software bill of materials plus build provenance attestation (SLSA-style) answers: these sources, these…
Compiler
Does this code compile? The cheapest and most certain sensor in the catalog. A compiler doesn’t just check syntax — it resolves imports, validates module structure, and produces an artifact.
Contract & Refinement Types
Behavioral guarantees checked before the code ever runs. Typestate systems, refinement types, and design-by-contract annotations (Eiffel-style pre/postconditions, Dafny requires/ensures) ask the…
Linter
Catches structural inconsistencies that are syntactically valid but semantically suspect. Lower oracle strength than a type checker, but faster feedback on style and common traps.
Model Checking
Exhaustive exploration of a system’s reachable states against a temporal property. Where a type checker proves a property holds for one step, and statically checked invariants prove a property holds…
Schema Validator
Structural coherence at the boundary of the system. OpenAPI/GraphQL schema validation, Terraform plan, Kubernetes admission validation, SQL parser/type checker — all of these answer: is this a valid…
Static Analysis
Pattern-matching and dataflow analysis over the source without executing it. Covers the space between a linter (style and local patterns) and a type checker (type soundness): null dereferences…
Theorem Proving
A machine-checked proof that a property holds for all inputs, not just the ones a test happened to exercise.
Type Checker
A Rust compiler saying expected Option<Foo>, found Foo is vastly more useful to an agent than “please reconsider whether this is correct.” This is the first and strongest form of computational…
Adjacent families
- Next: Behavioral — Does it do what we expect?
- All of them: the complete catalog (this family is also anchored there at /catalog/#structural).