Skip to content

Navigation Menu

Sign in
Sign up

Add Gale, Spar, Rivet to org profile README #5

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
avrabe wants to merge 1 commit into main
base: main
Choose a base branch
Loading
from update-org-profile-gale-ecosystem
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 62 additions & 15 deletions profile/README.md
View file Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand All @@ -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>
Expand All @@ -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">
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand All @@ -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>
Loading

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