diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml new file mode 100644 index 0000000..9693b00 --- /dev/null +++ b/.github/workflows/checks.yml @@ -0,0 +1,47 @@ +name: Checks + +on: + push: + branches: [main] + pull_request: + branches: [main] + +jobs: + ci: + name: ci + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate files exist + run: | + test -f profile/README.md + test -f profile/assets/pipeline.svg + + lint: + name: lint + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate markdown + run: | + # Check for broken relative image references + grep -oP 'src="\.\/[^"]+"|srcset="\.\/[^"]+"' profile/README.md | \ + sed 's/.*"\.\//profile\//' | sed 's/".*//' | \ + while read -r file; do + if [ ! -f "$file" ]; then + echo "Missing referenced file: $file" + exit 1 + fi + done + echo "All referenced files exist" + + test: + name: test + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate SVG + run: | + # Check SVG is well-formed XML + python3 -c "import xml.etree.ElementTree as ET; ET.parse('profile/assets/pipeline.svg')" + echo "SVG is valid" diff --git a/profile/README.md b/profile/README.md index fdede67..7aef11c 100644 --- a/profile/README.md +++ b/profile/README.md @@ -2,325 +2,141 @@ # PulseEngine -### Infrastructure for AI and WebAssembly +Formally verified WebAssembly toolchain for safety-critical systems -*Exploring the intersection where AI agents interact safely with real-world systems through WebAssembly's security model* +  -
+![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) -![Rust](https://img.shields.io/badge/Rust-000000?style=flat&logo=rust&logoColor=white) -![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat&logo=webassembly&logoColor=white) -![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat&logo=bazel&logoColor=white) -![C++](https://img.shields.io/badge/C++-00599C?style=flat&logo=cplusplus&logoColor=white) +  -[View Repositories](https://github.com/orgs/pulseengine/repositories) • [Documentation](#project-details) +[   Repositories   ](https://github.com/orgs/pulseengine/repositories)    [   Documentation   ](https://docs.rs/pulseengine-mcp-protocol)    [   Examples   ](https://github.com/pulseengine/wasm-component-examples) - - -
- -## What We're Building - -PulseEngine develops infrastructure at the intersection of AI and WebAssembly, ranging from WASI proposals to production-tested implementations. Our work focuses on enabling AI systems to safely interact with real-world applications through WebAssembly's capability-based security model. - -
- -## Core Infrastructure - - - - - - -
- -### WebAssembly Runtime -**[wrt](https://github.com/pulseengine/wrt)** +
+ Kiln + · + Meld + · + Loom + · + Synth + · + Sigil +
-Safety-critical WebAssembly runtime with Component Model support. 22+ interconnected crates designed for automotive (ASIL-D), aerospace (DO-178C), and medical (IEC 62304) applications. - -**Architecture** -Core execution engine, formal verification with 227 Kani harnesses, capability-based memory system, no_std compatibility - -**Development Stage** -Advanced beta - foundational infrastructure production-grade, core execution engine under active development - -		 - -### MCP Framework -**[mcp](https://github.com/pulseengine/mcp)** + -Rust framework for building Model Context Protocol servers. Extracted from production home automation deployment with 30+ tools. 12 modular crates covering protocol, security, auth, and monitoring. +  -**Features** -Complete MCP 2025-06-18 implementation, stdio/HTTP/WebSocket transports, 1,071 test functions, 80% code coverage +## The Pipeline -**Development Stage** -Production-ready beta (v0.13.0) - actively used in real systems, published to crates.io +Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals. -
- -
+
+PulseEngine Pipeline: .wasm → Meld (fuse) → Loom (optimize) → Synth (transpile) → Kiln (fire) — with Sigil attestation at every stage +
-## Build & Development Tools + 
-### Bazel Rules -**[rules_wasm_component](https://github.com/pulseengine/rules_wasm_component)** - -Modern Bazel rules for WebAssembly Component Model development. Supports Rust, Go, C++, and JavaScript with multi-profile builds and 73% faster compilation. - -**Highlights** -87 Starlark files, 415+ rule definitions, 30+ working examples, hermetic builds, OCI publishing, component signing +### [Meld](https://github.com/pulseengine/meld) -**Development Stage** -Beta → production-ready (v1.0.0) - comprehensive CI/CD, suitable for production with v2.0 planned +Statically fuses multiple WebAssembly P2/P3 components into a single core module. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time — runtime linking eliminated entirely. Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness. -### WebAssembly Signing -**[wsc](https://github.com/pulseengine/wsc)** +### [Loom](https://github.com/pulseengine/loom) -Enhanced WebAssembly signing toolkit with Rekor verification, based on wasmsign2. Bazel integration, keyless signing, WIT Component Model support. - -**Security** -Checkpoint-based verification, key fingerprint validation, origin verification, cross-shard attack prevention - -**Development Stage** -Active development - core signing/verification functional, Rekor validation operational +Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through SMT translation validation and mechanized proofs. Includes a fused mode purpose-built for Meld output.
-### WebAssembly Optimizer -**[loom](https://github.com/pulseengine/loom)** - -WebAssembly optimizer built with Cranelift's ISLE DSL. Declarative optimization rules with stateful dataflow analysis for constant propagation and memory optimization. +### [Synth](https://github.com/pulseengine/synth) -**Approach** -Novel contribution: extends ISLE's pure functional term rewriting with stateful tracking of locals and memory state - -**Development Stage** -Proof of concept - 40+ operations, demonstrates feasibility of ISLE-based WASM optimization +Transpiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations for provably optimal native code. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation. Translation validation ensures the transpiled output faithfully preserves WebAssembly semantics. -### File Operations -**[bazel-file-ops-component](https://github.com/pulseengine/bazel-file-ops-component)** - -Universal file operations for Bazel via WebAssembly components. Dual implementation (TinyGo for security, Rust for performance) with WASM sandboxing. +### [Kiln](https://github.com/pulseengine/kiln) -**Cross-Platform** -Replaces platform-specific scripts with sandboxed components working identically on Linux, macOS, Windows +![no_std](https://img.shields.io/badge/no__std-compatible-654FF0?style=flat-square&labelColor=1a1b27) -**Development Stage** -Active development - security model established, integration with rules_wasm_component ongoing +WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture for embedded, automotive, medical, and aerospace environments. Bounded allocations, deterministic execution, and memory safety through bounded model checking and formal verification.
-
+  -## AI Integration +### [Sigil](https://github.com/pulseengine/sigil) — Supply Chain Security - - - - - -
+![Sigstore](https://img.shields.io/badge/Sigstore-keyless_signing-654FF0?style=flat-square&labelColor=1a1b27) +![SLSA](https://img.shields.io/badge/SLSA-L4_provenance-00C853?style=flat-square&labelColor=1a1b27) -### AI-Native Graphical Modeling -**[glsp-mcp](https://github.com/pulseengine/glsp-mcp)** +The cryptographic backbone of the pipeline. Every stage — fusion, optimization, compilation — creates a signed transformation attestation recording what changed, which tool version ran, and cryptographic hashes of inputs and outputs. The full chain is verifiable end-to-end. -First implementation of Graphical Language Server Protocol using MCP. Enables AI agents to create and manipulate diagrams through natural language with WebAssembly component execution. +Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool version and hash constraints. Hardware security via TPM 2.0. Offline verification for air-gapped embedded environments. IoT device provisioning with pre-provisioned trust bundles. All signatures embedded directly in WebAssembly modules — no external registry required. -**Stack** -Rust backend (23,722 lines), TypeScript frontend (39,571 lines), wasmtime 24.0 runtime, multi-database layer (PostgreSQL, InfluxDB, Redis) +  -**Demo** -15+ ADAS components showing automotive system simulation with YOLOv5n neural network integration +> [!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. -**Development Stage** -Advanced MVP/beta - core features functional, production path identified +  - +
+Build & Verification -### WASI-MCP Proposal -**[wasi-mcp](https://github.com/pulseengine/wasi-mcp)** +  -Proposed WebAssembly System Interface API for Model Context Protocol, targeting WASI Preview3. Complete typed WIT interfaces mapping MCP protocol operations. +- [**rules_wasm_component**](https://github.com/pulseengine/rules_wasm_component) — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript +- [**rules_rocq_rust**](https://github.com/pulseengine/rules_rocq_rust) — Bazel rules for Rocq theorem proving and Rust formal verification with hermetic Nix toolchains +- [**rules_verus**](https://github.com/pulseengine/rules_verus) — Bazel rules for Verus Rust verification +- [**rules_moonbit**](https://github.com/pulseengine/rules_moonbit) — Bazel rules for MoonBit with hermetic toolchain support -**Coverage** -Full MCP 2025-06-18 specification - resources, tools, prompts, streaming, pagination, notifications +
-**Approach** -Protocol-faithful design following successful WASI proposals (wasi-http, wasi-filesystem patterns) +
+AI & MCP -**Development Stage** -Phase 0 pre-proposal - WIT interfaces complete, seeking stakeholder feedback for Phase 1 +  -
+- [**mcp**](https://github.com/pulseengine/mcp) — Rust framework for building Model Context Protocol servers and clients, published to crates.io +- [**glsp-mcp**](https://github.com/pulseengine/glsp-mcp) — AI-native graphical modeling with MCP integration and WebAssembly component execution +- [**wasi-mcp**](https://github.com/pulseengine/wasi-mcp) — Proposed WASI API for Model Context Protocol, targeting Preview 3 standardization -
+ -## Production MCP Servers +
+Developer Tools - - - - - - -
+  -### WindRiver Studio -**[studio-mcp](https://github.com/pulseengine/studio-mcp)** +- [**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 +- [**moonbit_checksum_updater**](https://github.com/pulseengine/moonbit_checksum_updater) — Native MoonBit checksum management with GitHub API integration -MCP server for WindRiver Studio CLI with Pipeline Management integration, intelligent caching, multi-instance authentication. + -**Status:** Production-ready -**Published:** npm (@pulseengine/studio-mcp-server) - - - -### Time & Date -**[timedate-mcp](https://github.com/pulseengine/timedate-mcp)** - -Comprehensive time operations with timezone support, format detection, timezone conversion, built with chrono-tz. - -**Status:** Production-ready -**Published:** npm (@pulseengine/timedate-mcp-server) - - - -### Template Server -**[template-mcp-server](https://github.com/pulseengine/template-mcp-server)** - -Automated template for creating MCP servers with PulseEngine framework. Example tools, resources, CI/CD workflows. - -**Purpose:** Developer onboarding -**Features:** Auto-setup script, validation, multi-platform binaries - -
- -
- -## Architecture Overview - -Our projects form an integrated ecosystem for AI-WebAssembly development: - -``` -┌─────────────────────────────────────────────────────────┐ -│ AI Integration Layer │ -│ • glsp-mcp: AI-native applications │ -│ • studio-mcp, timedate-mcp: Production servers │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ Protocol & Interface Layer │ -│ • mcp: Rust framework for MCP servers │ -│ • wasi-mcp: Standardization for WASI ecosystem │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ WebAssembly Runtime Layer │ -│ • wrt: Safety-critical WASM runtime │ -│ • loom: Optimization engine │ -│ • wsc: Component signing & verification │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ Build & Developer Tools │ -│ • rules_wasm_component: Bazel integration │ -│ • bazel-file-ops-component: Cross-platform operations │ -│ • template-mcp-server: Quick start templates │ -└─────────────────────────────────────────────────────────┘ -``` - -
- -## Vision & Focus Areas - -We're exploring what becomes possible when AI systems can safely interact with real-world systems through WebAssembly's security sandbox. - -| Focus Area | What We're Building | -|------------|---------------------| -| **Safety-Critical Systems** | Infrastructure for automotive (ASIL-D), medical (IEC 62304), and industrial applications with formal verification and certification frameworks | -| **AI-Native Development** | Tools treating AI agents as first-class participants - from diagram generation to build system integration | -| **Secure Integration** | Capability-based security allowing AI to control physical systems in vehicles, factories, and homes with verifiable safety properties | -| **Universal Portability** | Same code from microcontrollers to cloud infrastructure through WebAssembly's platform independence | - -
- -## Development Maturity - -Our projects span different maturity stages, from proposals to production: - -| Stage | Projects | Characteristics | -|-------|----------|-----------------| -| **🚀 Production** | mcp framework, studio-mcp, timedate-mcp | Published to registries, real-world deployments, comprehensive testing | -| **🔄 Advanced Beta** | wrt runtime, rules_wasm_component | Near-complete features, extensive infrastructure, production-quality tooling | -| **🚧 Active Development** | glsp-mcp, wsc, bazel-file-ops-component | Core features functional, integration ongoing, clear production path | -| **📝 Proposals & Research** | wasi-mcp, loom | Standards work, proof-of-concept implementations, seeking feedback | -| **🛠️ Developer Tools** | template-mcp-server | Onboarding and productivity tools | - -
- -## Project Metrics - -Based on comprehensive codebase analysis: - -| Repository | Language | Lines of Code | Commits | Test Coverage | Stage | -|------------|----------|---------------|---------|---------------|-------| -| wrt | Rust | 428,004 | 743 | 100+ test files, 227 Kani harnesses | Advanced Beta | -| mcp | Rust | 102,000 | 317 | 1,071 tests, 80% coverage enforced | Production Beta | -| glsp-mcp | Rust/TypeScript | 63,293 | 221 | Integration tests, UI demos | Advanced MVP | -| rules_wasm_component | Starlark/Rust | 252 files | 519 | 46 test builds, CI/CD | Beta → Production | -| wasi-mcp | WIT | - | - | Spec-complete | Phase 0 Proposal | -| studio-mcp | Rust | - | - | Production deployment | Production | -| wsc | Rust | - | - | Core functional | Active Dev | - -
- -## The Opportunity - -Traditional AI systems operate in isolation from real-world systems. WebAssembly's security model offers a path to safely bridge this gap. By treating AI agents as first-class citizens in our infrastructure, we're working toward systems where: - -- AI safely controls physical systems in vehicles, factories, and homes through verified WebAssembly components -- Developers build AI-aware applications with cryptographic security guarantees and formal verification -- Code runs consistently from embedded microcontrollers to cloud deployments with identical security properties -- Component composition enables complex AI workflows with modular, auditable security boundaries - -
- -## Technical Foundation - -**Languages:** Rust (primary), C++, Go, JavaScript/TypeScript -**WebAssembly:** Component Model, WASI Preview2/3, wasmtime runtime -**Build Systems:** Bazel (bzlmod), Cargo workspaces -**Safety:** Formal verification (Kani), ASIL-D compliance frameworks, capability-based security -**AI Integration:** Model Context Protocol, Ollama LLM, WASI-NN -**Standards:** Active participation in WASI standardization - -
+  ---
-*Work in progress. All projects under active development.* - -**[Explore Repositories →](https://github.com/orgs/pulseengine/repositories)** | **[MCP Framework Docs](https://docs.rs/pulseengine-mcp-protocol)** - -Built with a focus on safety, security, and enabling new possibilities at the intersection of AI and WebAssembly +Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore
diff --git a/profile/assets/pipeline.svg b/profile/assets/pipeline.svg new file mode 100644 index 0000000..6ad59eb --- /dev/null +++ b/profile/assets/pipeline.svg @@ -0,0 +1,66 @@ + + + + + sigil · attest · sign · verify + + + + .wasm + + + + + + Meld + fuse + + + + + + + + Loom + optimize + + + + + + + + Synth + transpile + + + + + + + + Kiln + fire +