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. + + @@ -48,12 +57,36 @@ Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals. - +
Spar
model		 →  .wasm  →  Meld
fuse		Kiln
fire
sigil · attest · sign · verifygale · 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