pulseengine
- 15 followers
- Germany
- https://pulseengine.eu
A WebAssembly Component Model toolchain for safety-critical systems, with formally verified components
Components are composed at build time and lowered to native code — the interface boundaries exist while you build and are gone when you ship.
components ──▶ meld ──▶ loom ──▶ synth ──▶ native
fuse optimize compile
kiln — interpret, on host or device
Everything the pipeline produces is signed and attested by sigil; everything it claims is traced by rivet.
| meld | Statically fuses WebAssembly components into one core module — import resolution, index-space merging, canonical-ABI adapter generation at build time, so nothing links at runtime. |
| loom | WebAssembly optimizer. Each rewrite is checked by SMT translation validation per run — a validated pass, not a verified tool. |
| synth | Transcodes WebAssembly to native ARM and RISC-V via program synthesis, targeting bare-metal Cortex-M/R. Declines an operation loudly rather than emitting code it cannot justify. |
| kiln | WebAssembly interpreter and runtime — full Component Model and WASI 0.2, with a no_std path for embedded. |
| sigil | Signing and attestation. Each stage records what changed, which tool version ran, and the hashes in and out; signatures embed in the module itself, and verification works offline for air-gapped devices. |
Different techniques, named separately — because they prove different things.
| rivet | Typed SDLC artifacts and traceability. Requirements, design, verification and their links as a checked graph; release readiness is a query over closed evidence rather than a date. |
| witness | MC/DC structural coverage measured on the lowered WebAssembly the runtime executes, not on the source it came from. |
| scry | Sound abstract interpretation — over-approximates, so it never misses a behaviour that can occur. Mechanized Rocq soundness proofs for specific domains. |
| ordeal | Certificate-checked QF_BV SMT. The solver is untrusted; an independent, formally-verified LRAT checker re-derives every UNSAT. |
| spar | Architecture models — AADL v2.3, SysML v2, CAN-DBC — with 30+ analyses including scheduling, fault trees and network-calculus timing bounds, and Lean proofs of the analyses themselves. |
| gale | Formally verified Rust replacements for Zephyr RTOS kernel primitives (Verus + Rocq + Lean), composing toward gust — an OS built from verified components. |
What "verified" means here. Verus (SMT, partial correctness, declared trusted base) · Kani (bounded model checking) · Rocq and Lean (specific theorems) · translation validation (per run, not the tool) · sound static analysis. Specific properties of specific components are proven. The toolchain as a whole is not, and we don't claim it is — see the preprint for where the gates are still weak.
| relay | Flight software as WebAssembly components, inspired by NASA's cFS. |
| wohl | OTA update and device lifecycle. |
| jess | Hardware integration — getting verified components onto real boards and into flight. |
Build & toolchain
- varve — pinned, signed, dated toolchain bundles; projects freeze on a layer and stay there (design)
- rules_wasm_component — Bazel rules for the Component Model across Rust, Go, C++, JavaScript
- rules_rocq_rust · rules_verus · rules_lean · rules_ordeal — hermetic Bazel rules for the proof and verification toolchains
- temper — GitHub App that holds repositories to organizational standards
- mcp — Rust framework for Model Context Protocol servers and clients
- template-mcp-server — scaffolding for a new MCP server
- wasm-component-examples — Component Model examples in C, C++, Go, Rust
- bazel-file-ops-component — cross-platform file operations for Bazel, as a Wasm component
Rust · WebAssembly Component Model · WASI 0.2 · Bazel · Verus · Rocq · Lean · Kani · Sigstore
Everything is work in progress. Claims are scoped to what is checked.
Pinned Loading
Repositories
- varve Public
varve — the PulseEngine toolchain layer manager: pinned, signed, dated toolchain bundles. One layer per release; read the one your project pins.
- gale Public
Gale — Formally verified Rust port of Zephyr RTOS kernel primitives. ASIL-D targeted, dual-track verification: Verus (SMT/Z3) + Rocq (theorem proving). Part of the PulseEngine toolchain.
- rivet Public
Rivet — SDLC traceability for safety-critical systems. Schema-driven artifact management, validation, and lifecycle linking. Part of the PulseEngine toolchain.
- scry Public
sound abstract interpretation for WebAssembly — the third DO-333 leg of the PulseEngine verification chain
- synth Public
Synth — WebAssembly-to-native compiler for ARM Cortex-M/R (Thumb-2/A32), RISC-V RV32, and AArch64, with mechanized Rocq correctness proofs, per-compilation translation validation, and sound WCET bounds. Part of the PulseEngine toolchain.
- jess Public
jess — hardware-integration & release-watch hub: brings falcon drone software onto hardware (HIL vs relay sim → real drone → flight). Tracked with rivet.
- rules_wasm_component Public
Bazel rules for WebAssembly Component Model development with multi-profile builds and dependency management
- sigil Public
Sigil — Supply chain security for WebAssembly. Embedded signatures, Sigstore keyless signing, SLSA provenance. Part of the PulseEngine toolchain.
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…