From 87af60996e33107210ec4803db794f00d56a2eab Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: 2026年3月15日 11:01:30 +0100 Subject: [PATCH] Add Gale, Spar, Rivet as first-class ecosystem members Promote the full PulseEngine stack beyond the WASM pipeline: Gale as the verified RTOS foundation layer, Spar for architecture analysis, and Rivet for SDLC traceability. Show how they connect end-to-end from kernel primitives through WebAssembly deployment. Also adds automator and thrum to Developer Tools. Co-Authored-By: Claude Opus 4.6 (1M context) --- profile/README.md | 77 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 62 insertions(+), 15 deletions(-) diff --git a/profile/README.md b/profile/README.md index ea86052..21ab76d 100644 --- a/profile/README.md +++ b/profile/README.md @@ -2,7 +2,7 @@ # PulseEngine -Formally verified WebAssembly toolchain for safety-critical systems +Formally verified toolchain for safety-critical systems — from RTOS kernel to WebAssembly deployment @@ -10,12 +10,15 @@ ![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) [ Repositories ](https://github.com/orgs/pulseengine/repositories) [ Website ](https://pulseengine.eu) [ Examples ](https://github.com/pulseengine/wasm-component-examples)
+ Gale + · Kiln · Meld @@ -25,18 +28,24 @@ Synth · Sigil + · + Spar + · + Rivet
-## 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.
+ Spar
model + → .wasm → Meld
fuse @@ -48,12 +57,36 @@ Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals. Kiln
fire
- sigil · attest · sign · verify + gale · verified RTOS kernel | sigil · attest · sign · verify | rivet · trace · comply
+## Foundation Layer + + +
+ + +### [Gale](https://github.com/pulseengine/gale) — 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. + + +
+ + + + +## WebAssembly Pipeline +
@@ -104,24 +137,36 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio -> [!NOTE] -> **Correctness at every layer** — 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 - + +
+ + +### [Spar](https://github.com/pulseengine/spar) — 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. + + + + +### [Rivet](https://github.com/pulseengine/rivet) — SDLC Traceability -
-Safety-Critical Systems +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. + + +
+ -- [**gale**](https://github.com/pulseengine/gale) — Formally verified Rust port of Zephyr RTOS kernel primitives for ASIL-D, dual-track Verus and Rocq verification -- [**spar**](https://github.com/pulseengine/spar) — AADL v2.2 architecture analysis toolchain — parser, semantic model, 30+ analyses, and LSP server -- [**rivet**](https://github.com/pulseengine/rivet) — Schema-driven SDLC artifact manager for requirements traceability and safety compliance +> [!NOTE] +> **Correctness at every layer** — 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. - +
-Build & Verification +Build & Verification Rules @@ -149,6 +194,8 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio +- [**automator**](https://github.com/pulseengine/automator) — Toolchain orchestrator for autonomous AI development, verification gates, and functional safety traceability +- [**thrum**](https://github.com/pulseengine/thrum) — Gate-based pipeline orchestrator for autonomous AI-driven development - [**temper**](https://github.com/pulseengine/temper) — GitHub App that hardens repositories to organizational standards - [**wasm-component-examples**](https://github.com/pulseengine/wasm-component-examples) — Working examples for Component Model development in C, C++, Go, and Rust - [**bazel-file-ops-component**](https://github.com/pulseengine/bazel-file-ops-component) — 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
-Rust · WebAssembly Component Model · WASI 0.2 · 0.3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore +Rust · WebAssembly Component Model · WASI 0.2 · 0.3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore · AADL · Zephyr RTOS

AltStyle によって変換されたページ (->オリジナル) /