Add Gale, Spar, Rivet to org profile README

profile/README.md

@@ -2,20 +2,23 @@
 
 # PulseEngine
 
-<sup>Formally verified WebAssembly toolchain for safety-critical systems</sup>
+<sup>Formally verified toolchain for safety-critical systems — from RTOS kernel to WebAssembly deployment</sup>
 
 &nbsp;
 
 ![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27)
 ![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27)
 ![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat-square&logo=bazel&logoColor=white&labelColor=1a1b27)
 ![Formally Verified](https://img.shields.io/badge/Formally_Verified-00C853?style=flat-square&logoColor=white&labelColor=1a1b27)
+![ASIL-D](https://img.shields.io/badge/ASIL--D-targeted-E65100?style=flat-square&labelColor=1a1b27)
 
 &nbsp;
 
 [<kbd> &nbsp; Repositories &nbsp; </kbd>](https://github.com/orgs/pulseengine/repositories) &nbsp;&nbsp; [<kbd> &nbsp; Website &nbsp; </kbd>](https://pulseengine.eu) &nbsp;&nbsp; [<kbd> &nbsp; Examples &nbsp; </kbd>](https://github.com/pulseengine/wasm-component-examples)
 
 <h6>
+  <a href="https://github.com/pulseengine/gale">Gale</a>
+  ·
   <a href="https://github.com/pulseengine/kiln">Kiln</a>
   ·
   <a href="https://github.com/pulseengine/meld">Meld</a>
@@ -25,18 +28,24 @@
   <a href="https://github.com/pulseengine/synth">Synth</a>
   ·
   <a href="https://github.com/pulseengine/sigil">Sigil</a>
+  ·
+  <a href="https://github.com/pulseengine/spar">Spar</a>
+  ·
+  <a href="https://github.com/pulseengine/rivet">Rivet</a>
 </h6>
 
 </div>
 
 &nbsp;
 
-## The Pipeline
+## The Full Stack
 
-Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.
+Gale hardens. Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals. Spar models. Rivet traces.
 
 <table align="center">
 <tr>
+  <td align="center"><a href="https://github.com/pulseengine/spar"><strong>Spar</strong><br><sub>model</sub></a></td>
+  <td align="center">&nbsp;→&nbsp;</td>
   <td align="center"><code>.wasm</code></td>
   <td align="center">&nbsp;→&nbsp;</td>
   <td align="center"><a href="https://github.com/pulseengine/meld"><strong>Meld</strong><br><sub>fuse</sub></a></td>
@@ -48,12 +57,36 @@ Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.
   <td align="center"><a href="https://github.com/pulseengine/kiln"><strong>Kiln</strong><br><sub>fire</sub></a></td>
 </tr>
 <tr>
-  <td colspan="9" align="center"><sub><a href="https://github.com/pulseengine/sigil">sigil</a> · attest · sign · verify</sub></td>
+  <td colspan="11" align="center"><sub><a href="https://github.com/pulseengine/gale">gale</a> · verified RTOS kernel &nbsp;&nbsp;|&nbsp;&nbsp; <a href="https://github.com/pulseengine/sigil">sigil</a> · attest · sign · verify &nbsp;&nbsp;|&nbsp;&nbsp; <a href="https://github.com/pulseengine/rivet">rivet</a> · trace · comply</sub></td>
 </tr>
 </table>
 
 &nbsp;
 
+## Foundation Layer
+
+<table>
+<tr>
+<td width="100%" valign="top">
+
+### [Gale](https://github.com/pulseengine/gale) &mdash; Verified RTOS Kernel Primitives
+
+![ASIL-D](https://img.shields.io/badge/ASIL--D-targeted-E65100?style=flat-square&labelColor=1a1b27)
+![Verus](https://img.shields.io/badge/Verus-SMT%2FZ3-00C853?style=flat-square&labelColor=1a1b27)
+![Rocq](https://img.shields.io/badge/Rocq-theorem_proving-654FF0?style=flat-square&labelColor=1a1b27)
+
+Formally verified Rust replacement for Zephyr RTOS kernel primitives. Nine kernel objects — semaphore, mutex, condition variable, message queue, stack, pipe, timer, memory slab, and event — verified through dual-track formal methods: Verus (SMT/Z3) for functional correctness and Rocq (theorem proving) for deeper refinement properties. Drop-in replacement via C FFI shims; all upstream Zephyr kernel tests pass unchanged on qemu_cortex_m3.
+
+**Gale provides the verified foundation that Kiln runs on** — formally proven kernel primitives underneath the WebAssembly runtime, closing the verification gap from hardware abstraction to application deployment.
+
+</td>
+</tr>
+</table>
+
+&nbsp;
+
+## WebAssembly Pipeline
+
 <table>
 <tr>
 <td width="50%" valign="top">
@@ -104,24 +137,36 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio
 
 &nbsp;
 
-> [!NOTE]
-> **Correctness at every layer** &mdash; Rocq mechanized proofs, Kani bounded model checking, Z3 SMT verification, and Verus Rust verification are used across the toolchain — not confined to individual projects. Sigil attestation chains bind it all together. No transformation ships without a proof.
+## Systems Engineering
 
-&nbsp;
+<table>
+<tr>
+<td width="50%" valign="top">
+
+### [Spar](https://github.com/pulseengine/spar) &mdash; Architecture Analysis
+
+AADL v2.2 toolchain in Rust — full parser, semantic model, 30+ architectural analyses, and LSP server. Models system architectures (threads, processes, devices, buses, memory) and validates them against safety constraints before a single line of implementation code is written. Feeds architectural decisions into the pipeline.
+
+</td>
+<td width="50%" valign="top">
+
+### [Rivet](https://github.com/pulseengine/rivet) &mdash; SDLC Traceability
 
-<details open>
-<summary><b>Safety-Critical Systems</b></summary>
+Schema-driven artifact manager for requirements traceability and safety compliance. Manages the full lifecycle from stakeholder needs through system requirements, software requirements, design, implementation, and verification — with bidirectional trace links at every level. 271 managed artifacts across the Gale project alone.
+
+</td>
+</tr>
+</table>
 
 &nbsp;
 
-- [**gale**](https://github.com/pulseengine/gale) &mdash; Formally verified Rust port of Zephyr RTOS kernel primitives for ASIL-D, dual-track Verus and Rocq verification
-- [**spar**](https://github.com/pulseengine/spar) &mdash; AADL v2.2 architecture analysis toolchain — parser, semantic model, 30+ analyses, and LSP server
-- [**rivet**](https://github.com/pulseengine/rivet) &mdash; Schema-driven SDLC artifact manager for requirements traceability and safety compliance
+> [!NOTE]
+> **Correctness at every layer** &mdash; Rocq mechanized proofs, Kani bounded model checking, Z3 SMT verification, and Verus Rust verification are used across the toolchain — not confined to individual projects. Gale's dual-track verification (Verus + Rocq) proves kernel correctness. Sigil attestation chains bind it all together. No transformation ships without a proof.
 
-</details>
+&nbsp;
 
 <details>
-<summary><b>Build & Verification</b></summary>
+<summary><b>Build & Verification Rules</b></summary>
 
 &nbsp;
 
@@ -149,6 +194,8 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio
 
 &nbsp;
 
+- [**automator**](https://github.com/pulseengine/automator) &mdash; Toolchain orchestrator for autonomous AI development, verification gates, and functional safety traceability
+- [**thrum**](https://github.com/pulseengine/thrum) &mdash; Gate-based pipeline orchestrator for autonomous AI-driven development
 - [**temper**](https://github.com/pulseengine/temper) &mdash; GitHub App that hardens repositories to organizational standards
 - [**wasm-component-examples**](https://github.com/pulseengine/wasm-component-examples) &mdash; Working examples for Component Model development in C, C++, Go, and Rust
 - [**bazel-file-ops-component**](https://github.com/pulseengine/bazel-file-ops-component) &mdash; WebAssembly-based cross-platform file operations for Bazel builds
@@ -162,6 +209,6 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio
 
 <div align="center">
 
-<sub>Rust · WebAssembly Component Model · WASI 0.2 · 0.3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore</sub>
+<sub>Rust · WebAssembly Component Model · WASI 0.2 · 0.3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore · AADL · Zephyr RTOS</sub>
 
 </div>