Lambda Aitia is the software and SDLC causal-assurance contribution for the POO Flow ecosystem. It also owns the software Architecture Decision Record (ADR) module migrated from Lambda Episteme. It answers five questions about an engineering conclusion:
- What exactly is claimed?
- Which sources, assumptions, arguments and evidence support it?
- Which structural, temporal and causal relations justify that support?
- Which changes make the conclusion stale, unknown, conflicted or invalid?
- Which decisions and real effects must remain blocked until the resulting obligations are discharged again?
The project manages the justification and invalidation of conclusions. It is not a database of green verification results and it is not a generic knowledge graph.
lambda-aitia
Software/SDLC, ADR, NASA and GitOps sources
claims, assumptions, typed relations, obligations, evidence,
invalidation and assurance planning
^
|
lambda-episteme
optional non-SDLC vertical knowledge and decision-kind/ontology sources
|
v
POO Flow
POO-native composition, functional flow, graph substrate,
verifier/runtime handoff and effect boundary
This is a conceptual flow, not permission to collapse repository ownership. POO Flow core never imports a concrete Lambda contribution. Lambda Aitia may consume the complete reviewed POO Flow public mechanism library needed by its Software/SDLC implementation; dependency minimization is not an architectural goal. Applications own the explicit composition of Episteme, Aitia and POO Flow. Mounting this Git submodule does not import a module, activate a Profile, run a verifier, grant a capability, authorize a decision or execute an effect.
The production Python SDLC Runtime is maintained entirely under
bindings/python in this repository; it is not an example. POO Flow’s
packages/python-runtime remains the generic graph execution and lifecycle
mechanism and does not own Aitia semantics. Aitia Scheme is compiled AOT
behind an owned-byte C ABI. The Python project validates typed lifecycle
receipts and exposes them to downstream systems without reimplementing Scheme
decisions.
The initial semantic vocabulary is deliberately small:
Artifact Claim Assumption Observation Event Action Obligation Evidence Counterexample Finding Decision Effect
Relations are typed by plane. A generic edge(from, to) is not part of the
public model.
| Plane | Representative relations | Meaning |
|---|---|---|
| Provenance | derived-from, generated-by, cites, used | where a value came from |
| Structural dependency | depends-on, implements, tests, refines | what a change may affect |
| Temporal and causal | precedes, causal-parent, enables, prevents | what happened and why |
| Assurance | supports, discharges, defeats, invalidates | why a claim is or is not justified |
| Authority | authorizes, denies, requires-review | whether a decision may cross an effect boundary |
The planes have different admission and inference rules. In particular,
derived-from is not caused-by, temporal order is not causal proof,
structural reachability is not assurance closure, and evidence is not action
authority.
The first vertical slice is one fail-closed lifecycle:
source revision changes -> structural impact is computed -> affected assumptions and claims are selected -> dependent evidence becomes stale -> new obligations are planned -> the old decision loses authority -> the associated effect remains blocked
The slice succeeds only when receipts bind the subject, source revision, assumption set, claim, obligation, producer identity, tool identity, artifact digest and validity interval. Missing or conflicting facts remain explicit; they are never converted into an inferred success.
Lambda Aitia treats an Agent RFC as an executable assurance subject, not just a design document. The RFC states intended behavior and trust boundaries; ADRs close bounded choices; Aitia projects their claims, assumptions, dependencies, threats, obligations and evidence into a revision-bound Assurance Graph. POO Flow supplies the reusable Governance, Graph/Impact Graph, Temporal Causality, verification-adapter, authorization-provider and Runtime mechanisms used to evaluate that model.
Spec-first Agent work asks an Agent to follow a better specification. Specula uses Agents to derive and validate TLA+ models from system code so that deep concurrency bugs can be found and reproduced. Lambda Aitia addresses the next system-level question: after RFCs, code, formal models, proofs, policies, tests and runtime observations all exist, which exact conclusion is still justified for the current revision, what change invalidated it, which obligations must be rerun, and why must an Agent effect remain blocked?
Aitia therefore does not compete with Lean, TLA+, TLC, Cedar, Specula or POO Flow. It binds their distinct artifacts into a causal-assurance lifecycle without pretending that one tool’s success proves the others’ propositions.
| Work or project | Primary object | Main strength | Boundary relative to Aitia | Relationship |
|---|---|---|---|---|
| POO Flow Agentic Control Plane RFC suite | organization Bundle, Agent control plane, proof/evidence chain and effect token | establishes reusable mechanism, ownership and authority boundaries | intentionally does not own Aitia’s Software/SDLC claims or assurance policy | POO Flow is the full public mechanism Library on which Aitia is built |
| Agent RFC / specification-first Agent development | human-reviewed intent, constraints and implementation plan | gives Agents an explicit architecture and acceptance target instead of an ad hoc prompt | a document does not establish current evidence, invalidation closure, authorization or execution | Aitia turns RFC clauses and revisions into typed claims, threats and obligations |
| Specula (paper) | code-derived TLA+ specification, invariants, traces and reproduced bugs | autonomous specification generation, model checking, trace alignment and concrete bug reproduction | concentrates on discovering implementation/model violations; it is not a cross-tool evidence, policy and effect-authority ledger | a Specula run can satisfy Aitia TLA+/replay obligations when its artifacts are identity-bound and admitted |
| Causal Software Engineering | lifecycle-wide causal models, assumptions and counterfactual diagnosis | provides the broader research vision for causal reasoning throughout software engineering | a vision and roadmap do not by themselves define Aitia’s POO objects, revision receipts or Runtime gate | Aitia is an executable contribution pursuing this direction with typed relation planes and invalidation |
| Conventional CI/CD and test dashboards | jobs, statuses, logs and deployment stages | repeatable automation and immediate regression signals | a green result usually does not encode the complete subject, assumption, revision, causal support or downstream invalidation graph | Aitia consumes exact test/build receipts as evidence rather than treating green status as authority |
| Lean, TLA+/TLC and Cedar used independently | theorem, checked state space or policy decision | strong, specialized reasoning inside a clearly defined formal boundary | none alone proves model-code alignment, evidence freshness, current authorization and effect completion | Aitia keeps the propositions separate and joins only digest-bound admitted receipts |
The comparison is about responsibility rather than feature count. Aitia’s distinctive unit is the current, revision-bound justification of a conclusion and its invalidation trajectory across the whole SDLC. Its value is the composition of specialized evidence with explicit unknown and authority boundaries, not a new theorem prover, model checker, policy engine or Graph implementation.
The threat model covers failures that ordinary pass/fail CI cannot distinguish:
- stale evidence is replayed after source, policy, assumption or tool changes;
- a cached Agent decision survives invalidation or revocation;
- an RFC claim, Lean statement, TLA+ model and Cedar policy refer to different revisions of the supposed same subject;
- tool exit success is admitted without exact input, environment and artifact bindings;
- a counterfactual or hypothesized trajectory is promoted into observed history;
- composition of independently valid components is assumed safe without a new composition obligation;
- an authorized intent is amplified, substituted or executed through an out-of-band Runtime path;
- an effect begins after revocation or is reported complete without an execution receipt.
No single formalism closes all of those threats. The layers have deliberately different propositions and trusted boundaries:
| Layer | Owns | Does not prove |
|---|---|---|
| Agent RFC and ADR | intent, vocabulary, trust boundary, decisions and required obligations | that an implementation, policy or runtime matches the documents |
| Aitia Assurance Graph | exact subject/revision bindings, typed support, invalidation, unresolved frontier and verification plan | temporal safety, authorization or effect execution |
| Lean | general laws such as freshness, monotone invalidation, modality preservation, no stale authority and composition obligations | that the current deployment supplied fresh facts or executed an effect |
| TLA+/TLC | bounded lifecycle transitions and adverse interleavings across change, invalidate, plan, verify, admit, decide, authorize and effect | universal theorem proof or production authorization |
| Cedar | an allow/deny decision for one identity-bound principal, action, resource, context, policy and entity snapshot | evidence freshness, proof construction, runtime conformance or external success |
| Runtime Host | one bounded execution attempt and its typed execution receipt | that missing proof or authorization may be inferred |
The intended evidence flow is:
Agent RFC / ADR / source revisions -> Aitia snapshot and threat/impact graph -> invalidation and typed verification obligations -> Lean proof receipts + TLA+/TLC model-check receipts + test/replay evidence -> evidence admission against the same snapshot -> Cedar projection and identity-bound authorization decision -> one bounded POO Flow Runtime execution -> execution receipt and post-effect evidence
Every arrow is digest- and revision-bound. Lean cannot replace Cedar, Cedar cannot replace TLA+, a TLC completion cannot replace runtime evidence, and a Runtime success cannot retroactively prove the RFC. Unknown, conflicted, stale, mismatched or unavailable inputs fail closed and remain visible in the receipt graph.
The current repository has executable snapshot/invalidation and modular Lean evidence. The complete TLA+ lifecycle, Cedar admission and Runtime effect gate remain explicit roadmap phases; their absence is not represented as closure. See RFC 0001, RFC 0002, RFC 0003 and ADR 0004.
- Public extension APIs are POO-native. The ordinary
aitia.sssurface selects the maintainedaitiaComposition and fills bounded Project slots; its macro lowers directly to those POO values. Prototype, C3 and slot-transform operators are exposed only when a user needs an advanced override. Neither layer uses raw alist DSLs or ad hoc patch languages. - Functional transformations are values first. Side effects live behind an explicit POO Flow verifier or runtime handoff.
- Native Scheme tests are never heap-unbounded: the Aitia Testing Interface defaults to 512 MiB, while complete NASA catalog and prepared-source-graph tests declare a bounded 2 GiB POO memory profile. POO Flow’s outer test launcher enforces the 512 MiB pre-import boundary before this profile loads.
- Relation planes remain disjoint and fail closed at their boundaries.
supported,violated,unknown,stale,conflicted,hypothesized,counterfactualandnot-applicableare first-class states.- A plan is not an execution, a receipt is not proof, proof is not current authority, and authority is not proof that an effect completed.
- Lambda Aitia owns Software Engineering/SDLC, NASA and GitOps source modules; its assurance kernel reasons over those declared facts without embedding a NASA- or provider-specific rule.
- Lambda Episteme retains non-SDLC vertical knowledge such as Healthcare and the independently owned decision-kind/ontology surfaces.
Lambda Aitia uses the same intentional dual-license contract as POO Flow:
Apache-2.0 AND LGPL-2.1-or-later. Recipients must comply with both licenses.
The machine-readable declaration and complete texts are maintained in
REUSE.toml, LICENSE and LICENSES/.
- RFC 0001 — Causal Assurance Core defines the architecture, invariants and ownership boundaries.
- RFC 0003 — Composition Value Interface defines the Jsonnet-style single-value
downstream file, the official
aitiaComposition and the advanced POO override boundary. - ADR contract and template defines standardized bounded decisions, lifecycle, RFC links and the non-authorizing assurance projection.
- ADR 0007 establishes POO Flow as Aitia’s reusable public mechanism library.
- ROADMAP defines phases, deliverables and completion gates.
- Software/SDLC integration inventory classifies the existing implementation as keep, reference, generalize or later migrate.
The repository has Phase 0 and Phase 1 evidence-partial work plus an active
Phase 2 snapshot/invalidation slice. ABI revision 2 and SdlcRuntime.plan()
form the first production Python runtime contract for the complete eight-stage
SDLC DAG. That plan remains inert: executable stage receipts, release
authority and completed effects are not claimed yet.