Repositories list

• 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 tran...

  rust arm embedded + 7

  rust arm embedded compiler webassembly riscv aarch64 wcet formal-verification pulseengine

  Rust

  •

  Apache License 2.0

  •0 0 forks•2 2 stars•11 11 issues•6 6 pull requests•Updated Sep 7, 2026Sep 7, 2026

• jess

  Public
  jess — hardware-integration & release-watch hub: brings falcon drone software onto hardware (HIL vs relay sim → real drone → flight). Tracked with rivet.

  Shell

  •0 0 forks•0 0 stars•5 5 issues•0 0 pull requests•Updated Sep 7, 2026Sep 7, 2026

• witness

  Public
  MC/DC-style branch coverage for WebAssembly components

  Rust

  •

  Apache License 2.0

  •0 0 forks•1 1 star•8 8 issues•4 4 pull requests•Updated Sep 7, 2026Sep 7, 2026

• varve

  Public
  varve — the PulseEngine toolchain layer manager: pinned, signed, dated toolchain bundles. One layer per release; read the one your project pins.

  Rust

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•40 40 issues•3 3 pull requests•Updated Sep 7, 2026Sep 7, 2026

• rivet

  Public
  Rivet — SDLC traceability for safety-critical systems. Schema-driven artifact management, validation, and lifecycle linking. Part of the PulseEngine toolchain.

  Rust

  •0 0 forks•2 2 stars•25 25 issues•1 1 pull request•Updated Sep 7, 2026Sep 7, 2026

• relay

  Public
  Formally verified flight software components for WebAssembly. Relay routes.

  Rust

  •

  Apache License 2.0

  •0 0 forks•2 2 stars•30 30 issues•5 5 pull requests•Updated Sep 7, 2026Sep 7, 2026

• 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 ...

  Rust

  •

  Apache License 2.0

  •0 0 forks•6 6 stars•21 21 issues•1 1 pull request•Updated Sep 7, 2026Sep 7, 2026

• kiln

  Public
  Kiln — WebAssembly runtime for safety-critical systems. Full Component Model and WASI 0.2 support. Part of the PulseEngine toolchain.

  rust embedded runtime + 5

  rust embedded runtime webassembly no-std wasi component-model pulseengine

  Rust

  •

  MIT License

  •1 1 fork•16 16 stars•22 22 issues•8 8 pull requests•Updated Sep 7, 2026Sep 7, 2026

• rules_wasm_component

  Public
  Bazel rules for WebAssembly Component Model development with multi-profile builds and dependency management

  toolchain rust webassembly + 3

  toolchain rust webassembly bazel component-model pulseengine

  Starlark

  •

  Apache License 2.0

  •0 0 forks•1 1 star•14 14 issues•8 8 pull requests•Updated Sep 7, 2026Sep 7, 2026

• pulseengine.eu

  Public
  The formally verified WebAssembly Component Model engine for safety-critical systems — org website and blog

  HTML

  •0 0 forks•0 0 stars•23 23 issues•0 0 pull requests•Updated Sep 7, 2026Sep 7, 2026

• meld

  Public
  Meld — Static WebAssembly component fusion. Part of the PulseEngine toolchain.

  rust webassembly fusion + 3

  rust webassembly fusion formal-verification component-model pulseengine

  Rust

  •

  Apache License 2.0

  •0 0 forks•10 10 stars•11 11 issues•0 0 pull requests•Updated Sep 7, 2026Sep 7, 2026

• mcp

  Public
  Rust framework for building Model Context Protocol servers and clients. Published to crates.io.

  rust framework mcp + 2

  rust framework mcp model-context-protocol pulseengine

  Rust

  •

  Apache License 2.0

  •0 0 forks•2 2 stars•1 1 issue•11 11 pull requests•Updated Sep 6, 2026Sep 6, 2026

• sigil

  Public
  Sigil — Supply chain security for WebAssembly. Embedded signatures, Sigstore keyless signing, SLSA provenance. Part of the PulseEngine toolchain.

  rust webassembly slsa + 3

  rust webassembly slsa supply-chain-security sigstore pulseengine

  Rust

  •0 0 forks•0 0 stars•23 23 issues•7 7 pull requests•Updated Sep 6, 2026Sep 6, 2026

• pulseengine-layers

  Public
  Layer assembly for the pulseengine realm — tool manifest and signed deposits. The assembler itself lives in pulseengine/varve.

  Python

  •0 0 forks•0 0 stars•2 2 issues•2 2 pull requests•Updated Sep 6, 2026Sep 6, 2026

• wohl

  Public
  Home supervision system built on PulseEngine. Wohl wahrt.

  Rust

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•5 5 issues•0 0 pull requests•Updated Sep 5, 2026Sep 5, 2026

• scry

  Public
  sound abstract interpretation for WebAssembly — the third DO-333 leg of the PulseEngine verification chain

  Rust

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•16 16 issues•1 1 pull request•Updated Sep 3, 2026Sep 3, 2026

• ordeal

  Public
  Ordeal — a pure-Rust, certificate-checked QF_BV SMT solver for the PulseEngine toolchain. Untrusted solver + formally-verified LRAT checker (CompCert pattern), ...

  Rust

  •

  Apache License 2.0

  •0 0 forks•1 1 star•2 2 issues•0 0 pull requests•Updated Sep 3, 2026Sep 3, 2026

• loom

  Public
  Loom — Formally verified WebAssembly optimizer. Part of the PulseEngine toolchain.

  rust webassembly optimizer + 4

  rust webassembly optimizer formal-verification isle cranelift pulseengine

  Rust

  •

  Apache License 2.0

  •0 0 forks•5 5 stars•20 20 issues•3 3 pull requests•Updated Sep 2, 2026Sep 2, 2026

• rules_lean

  Public
  Bazel rules for Lean 4 and Mathlib

  Starlark

  •0 0 forks•3 3 stars•3 3 issues•0 0 pull requests•Updated Aug 26, 2026Aug 26, 2026

• spar

  Public
  A compiler for system-architecture models — ingests AADL v2.3, SysML v2 & CAN/DBC into one semantic model; emits safety analysis, TSN timing bounds, and verifie...

  rust real-time compiler + 8

  rust real-time compiler webassembly aadl wcet safety-critical mbse tsn network-calculus + 1

  Rust

  •

  MIT License

  •1 1 fork•3 3 stars•18 18 issues•4 4 pull requests•Updated Aug 26, 2026Aug 26, 2026

• rules_ordeal

  Public
  Bazel rules for ordeal — certificate-checked QF_BV verification as a hermetic build gate

  Starlark

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•2 2 issues•0 0 pull requests•Updated Aug 20, 2026Aug 20, 2026

• .github

  Public
  0 0 forks•0 0 stars•1 1 issue•2 2 pull requests•Updated Aug 7, 2026Aug 7, 2026

• agora

  Public archive
  Real-time agent-coordination substrate — named agents coordinate on channels, every message a typed/signed/traceable fact. Augments the issue loop. WCM + NATS.

  Rust

  •0 0 forks•0 0 stars•0 0 issues•0 0 pull requests•Updated Aug 7, 2026Aug 7, 2026

• rules_rocq_rust

  Public
  Bazel rules for Rocq theorem proving and rocq-of-rust integration with hermetic Nix toolchains

  toolchain rust theorem-proving + 4

  toolchain rust theorem-proving bazel formal-verification rocq pulseengine

  Starlark

  •

  Other

  •0 0 forks•0 0 stars•6 6 issues•1 1 pull request•Updated Jul 22, 2026Jul 22, 2026

• wasm-tools

  Public
  CLI and Rust libraries for low-level manipulation of WebAssembly modules

  Rust

  •

  Apache License 2.0

  •348 348 forks•0 0 stars•2 2 issues•1 1 pull request•Updated Jun 22, 2026Jun 22, 2026

• wit-bindgen

  Public
  A language binding generator for WebAssembly interface types

  Rust

  •

  Apache License 2.0

  •286 286 forks•0 0 stars•3 3 issues•1 1 pull request•Updated Jun 21, 2026Jun 21, 2026

• rowan

  Public
  Rust

  •

  Apache License 2.0

  •87 87 forks•0 0 stars•0 0 issues•0 0 pull requests•Updated Jun 10, 2026Jun 10, 2026

• zephyr

  Public
  Primary Git Repository for the Zephyr Project. Zephyr is a new generation, scalable, optimized, secure RTOS for multiple hardware architectures.

  C

  •

  Apache License 2.0

  •9.9k 9.9k forks•0 0 stars•0 0 issues•0 0 pull requests•Updated May 29, 2026May 29, 2026

• example-kvs

  Public
  Eclipse-score persistency::kvs through the full pulseengine stack — rivet typed artifacts + spar AADL + WIT contract + witness MC/DC harness + sigil release man...

  wit aadl safety-critical + 7

  wit aadl safety-critical spar mbse iso-26262 rivet wasm-component pulseengine eclipse-score

  Rust

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•2 2 issues•2 2 pull requests•Updated May 25, 2026May 25, 2026

• playground-eclipse-score

  Public
  Eclipse S-CORE typed-traceability playground — 2985 sphinx-needs artifacts converted to rivet typed YAML, with falsification oracle and starter variant model. N...

  traceability safety-critical mbse + 7

  traceability safety-critical mbse requirements-engineering iso-26262 rivet sphinx-needs falsification eclipse-score asil-b

  Python

  •

  Apache License 2.0

  •0 0 forks•0 0 stars•2 2 issues•1 1 pull request•Updated May 24, 2026May 24, 2026