An open-source, Rust-based microkernel VMM unifying VMs, containers, and WebAssembly workloads with hardware-level GPU/NPU virtualization. Built for the AI era and the post-Broadcom/VMware era of infrastructure freedom.

An AI-native language and agentic compiler that turns declared intent, invariants, and constraints into formally verified Rust and Go code.

Open-source, AI-driven physical plant controller for hyperscale data centers — Rust edge agents, Go telemetry ingestion, and a burn-based RL thermal brain behind a common Hardware Abstraction Layer.

Write your UI once in Rust and render it anywhere: native/WASM canvas (egui+taffy), reactive DOM, semantic HTML, terminal UI (ratatui), JSON-LD/AI-agent schema, and an OS-webview desktop shell — served to the right client by a smart backend router.

A unified, cross-platform, zero-cost async I/O framework for Rust, abstracting io_uring, IOCP, and kqueue behind a single memory-safe API.

Rust workspace for building LLM-powered agents: unified streaming clients for OpenAI/Anthropic/Ollama, RAG pipeline (chunking, embedding, context management), vector store traits (Qdrant/Milvus/pgvector), tool-use macros, prompt templating, tokenization, agent memory, eval harness, and a mock server.

A proof-native, formally verified no_std Rust foundation for ESP32 — typestate-safe DMA/ISR, WCET-bounded telemetry, verified sleep transitions, constant-time crypto, and mesh state sync, proven with Kani.

Host-side verification, simulation, and analysis suite for proof-native ESP32 firmware — deterministic simulator, static stack analyzer, structured trace verifier, HIL orchestration, and cross-crate invariant checking for tpt-embedded-core.

A high-performance, zero-cost Rust toolkit for local AI. Features HuggingFace model caching, LoRA weight merging, safetensors I/O, and pure-Rust tokenization.

Dynamic-depth, symbolic-verified LLM inference in Rust — a from-scratch implementation of non-sequential transformer forward passes (arbitrary layer programs) with a lightweight router and a symbolic verifier for reasoning consistency, aimed at closing the 8B→32B quality gap without model compression.