Lab · Specification & verification
One surface for every behavioral expectation
Behavioral Constraint Surface (BCS) treats every requirement (traditionally split into “functional” and “non-functional”) as the same primitive: a governed, falsifiable constraint on observable system transitions. Intent (π), measurement (ω), decision boundary (φ), criticality (κ), and explicit capability scope (s) form the β-tuple; the `.bcs` language and observation adapters connect that model to pipelines, docs, and production diagnostics.
- Unified primitive: correctness, latency, security, privacy, and accessibility differ by what ω measures, not by incompatible requirement “types.”
- Continuous surface: locality |s|, observation domain, falsifier mode, and temporal binding are axes you slice for views; no privileged FR/CFR partition.
- Typed seam: adapters implement ω; falsify expressions type-check against measurement schemas before any environment runs.
- Progressive hardness: from documentation-only constraints → manual attestation → automated probes → continuous monitoring, without rewriting intent.
β = 5
Tuple fields
Predicate π, observation ω, falsifier φ, criticality κ, scope s; every construct in the DSL maps to one row of the tuple.
ω
Single integration seam
Only `observe … using` touches the running system; specification and falsification stay declarative and portable.
Lean
Formal core
Definitions and proof obligations live in Lean; MATH.md tracks the model. Discrepancies resolve in favor of the proof library.
Critique & reframing
Why the FR / CFR split stops being a useful model
The classic taxonomy is a surjection onto two labels. It throws away structure: migration SEO integrity, consent-gated analytics, and Core Web Vitals sit on seams the vocabulary was not designed to cut cleanly.
The split persists for good human reasons: Conway-aligned ownership, cognitive chunking, different verification clocks. Those are organizational heuristics, not boundaries in the system. When the specification layer encodes the split as ontology, cross-cutting expectations fracture across documents, backlogs, and test pyramids.
BCS keeps the heuristics for elicitation and replaces the modeling primitive: every expectation is a behavioral constraint; “functional vs quality” becomes a derived view over observation codomain and scope cardinality, not a type system for tickets.
Observation determines the traditional label
If ω maps transitions to booleans of correctness, you read “functional.” If ω returns milliseconds, you read “performance.” If ω returns authorization outcomes, you read “security.” The constraint shape is stable; the measurement varies.
That shift matters in practice: one meta-schema for gates, one graph model for coupling, one place to attach systemic diagnostics instead of parallel worlds for “stories” and “SLOs.”
Primitive
The behavioral constraint β
One row in the surface: five fields, one satisfaction story. Predicate and falsifier must agree for well-specified constraints.
| Name | Role | |
|---|---|---|
| π | Predicate | Behavioral assertion: what should hold over transitions. |
| ω | Observation | Measurement function T → V; the only field that binds to real probes, APIs, browsers, or humans. |
| φ | Falsifier | Pointwise or statistical decision boundary on values produced by ω. |
| κ | Criticality | must | should | could | must not, mapped to pipeline severity and governance weight. |
| s | Scope | Finset of capabilities the constraint spans; |s| is locality (systemic when > 1). |
Geometry
Axes of the constraint surface
Requirements occupy regions, not boxes. Each axis is a deliberate view; none is the “true type” of work.
Observable scope (locality)
|s|
Replaces: “Functional” vs “cross-functional”
Cardinality of touched capabilities. |s| = 1 reads as local; larger sets read as systemic: a continuous measure, not a binary bin.
Observation domain
codomain(ω)
Replaces: Requirement “category” lists
What V is (latency, enum, structured report) tells you how to visualize and compose gates; it is not a separate document taxonomy.
Falsifiability mode
pointwise | statistical
Replaces: Ad-hoc “aggregate OK?” rules
Per-sample thresholds vs decisions over lists of measurements are explicit in φ, so longitudinal and SLA-style constraints do not pretend to be unit tests.
Temporal binding
verify …
Replaces: Implicit “we check everything in CI”
immediate, deferred(d), longitudinal(w), on-event, continuous: constraints admit different clocks in the same surface.
Practice
Impact on traditional software engineering
| Practice area | Typical fracture | BCS stance |
|---|---|---|
| Requirements engineering | Parallel FR docs, NFR annexes, and Gherkin that strains on system-wide invariants. | Surfaces group constraints by iteration or boundary; criticality-first lines read as law, not ceremony. |
| Architecture & integration | Quality attributes float separately from features; traceability breaks at service boundaries. | Scope spans capabilities explicitly; coupling is scope overlap, so the same graph machinery serves risk and test planning. |
| Verification & QA | Different tools per concern; no shared notion of “satisfied” across teams. | sat(β, T_obs) unifies satisfaction; manual and automated observations share one status model. |
| CI / CD governance | Must-fix rules scattered in YAML, scripts, and policy wikis. | Compilation targets: blocking gates for must, warnings for should, scaffolding from the same `.bcs` source. |
| Operations & observability | SLAs live in monitoring; “spec” lives in Confluence, and drift is normal. | verify continuous elevates the same constraint from doc to probe schedule without changing π or φ. |
.bcs language
Declarative constraints, compilable surface
- The criticality keyword opens the statement with no Feature/Scenario wrapper.
- Each constraint is one β row: across, observe (+ optional using), falsify, verify.
- No Given/When/Then mandate: many constraints are observer-independent invariants, not single-actor narratives.
Surfaces compile to JSON/TS tuples, test stubs, documentation, coupling graphs, and CI severity from one source, with many projections.
surface iter-000-pre-launch
across property-access, privacy-compliance
must "No indexed URL returns 404 after migration"
across property-access
observe "Coverage + redirect audit"
using http.batch_probe {
urls: from "artifacts/legacy-urls.csv"
method: HEAD
follow: redirects
}
falsify count(responses where status = 404) = 0
verify immediateIntegration seam
Three layers, one contract
Specification (.bcs)
Criticality, scope, falsify, verify: pure, framework-agnostic declarations.
Observation (adapters)
Imperative modules implementing ObservationAdapter (HTTP, browser, API, CLI, manual.*), registered built-in, per-project, or via packages.
Falsification
Expressions consume measurements only and never reach into the system directly; type-checked against adapter output schemas at compile time.
Evaluation pipeline
Steps 1–3 are compile-time (fast feedback, no cluster required). Steps 4–6 run against the real system or human operators.
Parse
Extract κ, π, scope, observe/using, falsify, verify from the surface.
Resolve ω
Look up adapter kind, validate config; unknown adapter is a compile error.
Type-check φ
Field references in falsify must exist on the measurement schema.
Observe
Run adapter.observe with SystemContext (env, secrets, artifacts, clock, logger).
Falsify
Evaluate φ on measurements; produce satisfied / violated with evidence.
Govern
Apply κ: must blocks, should warns, could logs; must not carries inverted π, φ at must severity.
Progressive automation
Same constraint, increasing measurement fidelity
Documentation-only
Quoted observe text without `using` is still a valid surface: human verification, shared vocabulary.
Manual adapters
manual.checklist / manual.attestation records operator, timestamp, and structured pass/fail.
Automated adapters
Replace manual bindings with http.*, ga4.*, lighthouse.*, custom observers; π and φ stay put.
Continuous
The same constraint under verify continuous aligns production diagnostics and SLA monitors with the spec.
Author note
Systemic component diagnostics
When constraints span multiple capabilities (|s| > 1), violations are inherently cross-cutting: a privacy gate and an analytics pipeline fail together if consent state and network behavior disagree. BCS makes that overlap explicit instead of hiding it in separate test suites.
I use BCS in my own work as the spine between “what must stay true” and “how we observe it”, so diagnostics reports, coupling graphs, and gate configs are projections of one surface rather than three divergent sources of truth.
bcs-core / Lean
Formal model (Lean)
Transitions are typed as pre-state, event, post-state, elapsed time, and context. BehavioralConstraint packs V as the observation codomain; heterogeneous surfaces existentially quantify V per row.
Satisfaction generalizes pointwise and statistical falsifiers; gate nesting (aspiration → quality → deployment) is proven for homogeneous and heterogeneous specs. Coupling density ρ is graph-theoretic over scope overlap, which helps when reasoning about how “systemic” a release slice really is.
Caveats
BCS is a specification and verification model under active development; adapter ecosystems and compiler targets mature unevenly. The Lean library is the formal source of truth when prose and proofs disagree. This page is an interpretive synthesis for practitioners, not a normative replacement for package documentation.
Interested in constraint surfaces or diagnostics on your system?
Initiatives &
Research
Beyond my personal consultancy, I am actively building the future of software delivery and collaboration through these dedicated entities.
api.land
Curated infrastructure and building blocks for modern engineering teams. Providing the modules you need to build faster.
intelligence.space
A research lab re-imagining human-AI collaboration. Building an "Intelligent Space" for the entire lifecycle of systems engineering and learning itself.