README.md

# Sovereign Event Bus

![Sovereign Event Bus architecture and implementation status](docs/assets/seb-architecture.svg)

Sovereign Event Bus (SEB) is a multi-language reference implementation for
deterministic event coordination, policy-gated execution, human review, and
evidence-oriented delivery. The repository explores how an event can move from
an explicit authority envelope to an auditable outcome across Rust, Erlang,
Ada, Lean, and legacy enterprise adapters.

> [!IMPORTANT]
> SEB is under active hardening. It is not a production-ready event broker,
> cryptographic trust boundary, WORM store, or completed formal verification.
> The status tables below separate tested code from interfaces, prototypes, and
> open gates.

[Architecture](#architecture) | [Current status](#current-status) |
[Evaluate the code](#evaluate-the-code) | [Repository map](#repository-map) |
[BOB commands](#bob-commands) | [Production hardening](docs/PRODUCTION_HARDENING.md) |
[Developer guide](docs/DEVELOPER_GUIDE.md)

## Why this repository exists

SEB is organized around five engineering questions:

1. Can an event carry its intent, authority, evidence, and continuation state
   as one inspectable envelope?
2. Can routing and policy decisions be deterministic enough to reproduce?
3. Can native, managed, and legacy runtimes share a stable event contract?
4. Can high-impact transitions require an explicit human decision?
5. Can implementation evidence be connected to formal models without claiming
   more assurance than the evidence supports?

The codebase contains concrete experiments for each question. It does not yet
compose them into one deployable service.

## Current status

Status recorded on 2026-07-25 from the repository's default branch.

| Component | What is present | Current evidence | Open gate |
| --- | --- | --- | --- |
| Reasoning | Rust A2A events, traces, streaming buffers, and integration types | 18 library tests pass | The example target does not compile; transport, persistence, and real signatures are absent |
| Universe | Rust artifact manifests, indexes, search, and a compile-verify-merge model | 15 library tests pass | The example target does not compile; gate steps inspect metadata rather than invoking tools |
| Runtime | Erlang/OTP supervisors, agent FSM, partition manager, policy bridge, and kernel facade | Source and test modules are present | Runtime compile/test/release is not validated; the NIF and policy process are not operational |
| Kernel | Ada interfaces, an in-memory kernel body, WAL source, and a C NIF surface | Public interfaces and test-vector scaffolding are present | No portable build; persistence is disconnected; verification and key handling contain placeholders |
| Human review | Rust queue, audit log, and commit-gateway types | Workflow structure is present | The crate does not compile; authorization, durable storage, and gateway integration are incomplete |
| Lean verification | Lean models and proof attempts pinned to Lean 4.7.0 | Specifications are inspectable | The default build fails and proof files contain `sorry` or simplified cryptographic models |
| Enterprise adapters | RPG/ILE fiscal adapter, COBOL copybook, and PL/I declarations | Platform contracts and build notes are present | Not tested on IBM i or z/OS; wire layouts are not yet interoperable |
| Contracts and codegen | Rust, TypeScript, Python, Lean, and OpenAPI templates with shell generators | Templates are versioned | Generators are copy-oriented, output assumptions differ, and no conformance suite enforces parity |

The two passing Rust library suites are useful development baselines. They do
not constitute end-to-end, security, interoperability, or production evidence.

## Architecture

The intended event path is:

```text
producer
   |
   v
event envelope
   |
   v
authority and policy decision
   |
   v
deterministic routing
   |
   +----> bounded execution adapter
   |
   +----> human review when policy requires it
   |
   v
receipt, trace, and durable evidence
```

The repository implements these concerns in separate component experiments:

- `seb/contracts` defines candidate cross-language shapes.
- `seb/kernel` explores append, chain, offset, and segment interfaces.
- `seb/runtime` explores OTP supervision and per-agent coordination.
- `seb/reasoning` records reasoning-oriented A2A events and trace timelines.
- `seb/universe` indexes artifacts and models promotion gates.
- `seb/human_touch` models review and approval objects.
- `seb/verification/lean4` models selected invariants.
- `seb/adapters` documents legacy platform integration.

There is currently no executable that joins every box into one request path.
The canonical wire encoding, signature input, key authority, persistence
contract, and failure semantics must be unified before components can be
treated as one system.

## Evaluate the code

### Prerequisite

Install a Rust toolchain with Cargo. The repository has no root Cargo workspace,
so invoke each crate through its manifest.

```bash
git clone https://github.com/SNAPKITTYWEST/Sovereign-Event-Bus.git
cd Sovereign-Event-Bus

cargo test --manifest-path seb/reasoning/Cargo.toml --lib
cargo test --manifest-path seb/universe/Cargo.toml --lib
```

Expected baseline:

```text
seb/reasoning: 18 library tests pass
seb/universe:  15 library tests pass
```

Cargo will create local `target/` directories and may create crate-level lock
files. Build outputs are ignored by Git.

Do not use a successful library-only run to infer that examples or all targets
pass. These broader commands currently expose known integration failures:

```bash
cargo test --manifest-path seb/reasoning/Cargo.toml --all-targets --all-features
cargo test --manifest-path seb/universe/Cargo.toml --all-targets
cargo test --manifest-path seb/human_touch/Cargo.toml
```

The failures and ownership boundaries are cataloged in the
[developer guide](docs/DEVELOPER_GUIDE.md).

### Additional toolchains

Install only what is needed for the component being evaluated.

| Area | Required environment |
| --- | --- |
| Erlang runtime | Erlang/OTP and `rebar3` |
| Lean models | `elan`/Lean and `lake`; the project pins Lean and mathlib 4.7.0 |
| Ada kernel | GNAT/SPARK tooling, Erlang NIF headers, and the intended native crypto dependencies |
| Code generation | Bash, GNU Make, and Python 3; optional TypeScript and YAML validators |
| RPG adapter | IBM i with ILE RPG and DB2 objects described in the adapter guide |
| PL/I contract | z/OS Enterprise PL/I and site-specific JCL/link configuration |

Windows users should run shell tooling in a real Bash environment such as
Git Bash, MSYS2, or WSL. The scripts assume several GNU utilities and are not
PowerShell-native.

## Repository map

```text
.
|-- bob-shell/                    Development command wrappers
|-- docs/
|   |-- DEVELOPER_GUIDE.md       Build, test, and contribution workflows
|   |-- PRODUCTION_HARDENING.md  Readiness gates and operational criteria
|   `-- assets/                   Repository visuals
|-- seb/
|   |-- adapters/                RPG, copybook, and PL/I integration assets
|   |-- contracts/               Cross-language source templates
|   |-- human_touch/             Human-review Rust prototype
|   |-- kernel/                  Ada kernel and C Erlang NIF prototype
|   |-- reasoning/               Rust reasoning and trace library
|   |-- runtime/                 Erlang/OTP runtime prototype
|   |-- scripts/codegen/         Template expansion scripts
|   |-- universe/                Rust artifact-universe library
|   `-- verification/lean4/      Lean models and proof sources
|-- BOB_OPERATIONAL_CONTRACT.md
|-- BOB_TRUST_DEED_V1.md
`-- LICENSE
```

Layer numbers in historical documents are not fully consistent. This README
uses component names as the stable identifiers. References to an L0 master
specification or Idris implementation point to work that is not present in this
repository.

## Working with the components

### Reasoning

The reasoning crate exposes A2A event types, trace records, streaming support,
and integration structures from
[`seb/reasoning/src/lib.rs`](seb/reasoning/src/lib.rs).

```bash
cargo build --manifest-path seb/reasoning/Cargo.toml
cargo test --manifest-path seb/reasoning/Cargo.toml --lib
```

Trace storage and event streaming are process-memory structures. The current
signature field is not an Ed25519 implementation and must not be used as
authentication evidence.

### Universe

The universe crate exposes artifact manifests, an in-memory repository index,
and a model of compile-verify-merge gates from
[`seb/universe/src/lib.rs`](seb/universe/src/lib.rs).

```bash
cargo build --manifest-path seb/universe/Cargo.toml
cargo test --manifest-path seb/universe/Cargo.toml --lib
```

Gate steps currently validate metadata and simulated outcomes; they do not run
compilers, proof checkers, review services, or deployment systems.

### Erlang runtime

The intended local workflow is:

```bash
cd seb/runtime
rebar3 compile
rebar3 eunit
rebar3 dialyzer
```

These commands are targets to restore, not a passing baseline. The current
source has compile issues, the test functions are not discovered by EUnit, and
the Erlang facade does not load or match the C NIF interface.

### Lean verification

```bash
cd seb/verification/lean4
lake build
```

The project pins Lean 4.7.0 and mathlib 4.7.0. The default proof target
currently fails type checking, and several proof sources contain `sorry`.
Treat all proof certificates in the tree as historical development artifacts
until CI builds the declared theorem set with a zero-placeholder policy.

### Kernel and adapters

The Ada/C kernel and IBM adapter sources do not have a portable, tested build
entry point. Start with:

- [`seb/kernel/src/seb_kernel.ads`](seb/kernel/src/seb_kernel.ads) for the
  intended kernel API.
- [`seb/kernel/c/seb_kernel_nif.c`](seb/kernel/c/seb_kernel_nif.c) for the C NIF
  registry.
- [`seb/adapters/L4_ADAPTER_BUILD_GUIDE.md`](seb/adapters/L4_ADAPTER_BUILD_GUIDE.md)
  for target-platform assumptions.

Do not infer binary or wire compatibility from matching field names. Current
Ada, C test-vector, RPG, PL/I, Rust, Python, and TypeScript representations do
not yet share one validated canonical encoding.

## BOB commands

`bob-shell` contains development wrappers for common repository operations.
Invoke the scripts by filename from a Bash environment:

```bash
bash bob-shell/bob-build.sh
bash bob-shell/bob-test.sh
bash bob-shell/bob-audit.sh
bash bob-shell/bob-policy.sh
bash bob-shell/bob-proof.sh
bash bob-shell/bob-deploy.sh
```

| Command | Intended use | Important current behavior |
| --- | --- | --- |
| `bob-build.sh` | Dispatch component builds | Missing toolchains may be skipped; the report is not proof that every component built |
| `bob-test.sh` | Dispatch test suites | Deterministic mode sets environment variables but does not establish reproducibility by itself |
| `bob-audit.sh` | Produce file hashes and audit output | Requires GNU-style utilities; traversal, timestamps, and build files affect output |
| `bob-policy.sh` | Run a Prolog policy query | May create default governance files and executes a caller-supplied query |
| `bob-proof.sh` | Dispatch a proof backend | May create placeholder proof files; its generated certificate is not a production attestation |
| `bob-deploy.sh` | Package build output | Validation and sealing can be disabled; packaging is not deployment authorization |

These wrappers are operator conveniences, not a security boundary. Review their
working-tree mutations and generated reports before using them in automation.
See [`bob-shell/README.md`](bob-shell/README.md) and the
[developer guide](docs/DEVELOPER_GUIDE.md) for details.

## Failure modes to design for

The production plan treats the following as first-class scenarios:

| Scenario | Current behavior or risk |
| --- | --- |
| Process crash or restart | Several stores are in memory; recovery and replay are not demonstrated |
| Duplicate or replayed event | No shared nonce/idempotency store spans the components |
| Policy engine unavailable | The Erlang bridge can lack a live external process |
| Key compromise or rotation | No key authority, rotation protocol, revocation path, or historical-key policy is implemented |
| Partial append | WAL integration, atomic commit, and recovery evidence are incomplete |
| Partition rebalance | Current logic resets counters rather than transferring assignments |
| Human decision timeout | Durable queueing, escalation, authorization, and exactly-once commit are incomplete |
| Malformed or oversized envelope | A canonical encoding and cross-language conformance limits are not enforced |
| Short or non-ASCII identifiers | Some Rust diagnostic formatting uses fixed byte slices and can panic |
| Mixed-version deployment | There is no schema negotiation or compatibility matrix |

See [Production hardening](docs/PRODUCTION_HARDENING.md) for exit criteria,
required evidence, threat boundaries, release controls, and edge-case tests.

## Security and assurance

Until the hardening gates are complete:

- Do not expose SEB directly to untrusted networks.
- Do not use generated seals or certificates as legal, financial, or compliance
  evidence.
- Do not process secrets, regulated records, or irreversible production actions.
- Do not rely on BOB reports as attestations without independently validating
  their inputs and tool exits.
- Report non-sensitive defects through GitHub issues. Do not publish an
  undisclosed vulnerability before a private reporting channel is established.

The project needs an explicit security policy, supported-version policy, and
private disclosure route before a public production release.

## Development

The [developer guide](docs/DEVELOPER_GUIDE.md) covers:

- component-specific build and test commands;
- known failures and expected outputs;
- contract and wire-format ownership;
- generated files and cleanup;
- review requirements for security-sensitive changes; and
- the evidence required to change a status in this README.

Contributions should make the smallest coherent change, include tests at the
affected boundary, and update status claims only when a repeatable command or
artifact supports them.

## License

The repository is distributed under the
[Apache License 2.0](LICENSE). Some component metadata contains older license
labels; resolve those inconsistencies before packaging or redistributing an
affected component.