kani

Hard real-time Rust microkernel for brain-computer interfaces. #![no_std] on Cortex-M, EDF scheduling with Kani-verified WCRT bounds, zero-copy intent path, capability-based privacy by construction. ABI v1 — tandem with axonos-sdk.

DEX (Dalvik) decompiler. Parses, builds CFG, SSA via Braun, emits Java. Inverse emit_dex byte-identical on F-Droid (5,767 files). DEX v035–v041. Pure Rust.

Kani extension for supporting vision-language models (VLMs). Comes with model-agnostic support for GPT-Vision and LLaVA.

Saathi (साथी, “companion”) helps elders living alone stay safe and close to family, in their own language: tablets, check-ins, scam calls, help when it matters. An MCP server for Alexa+ and any MCP client, with a formally verified Rust/WASM core, post-quantum E2EE, passkeys and TPM-sealed keys. Try it: npx -y saathi-alexa

Free, ad-free, open-source Bangladeshi land unit converter — katha, bigha, shotangsho, decimal, gonda, kani, acre, square feet, square metre. বাংলা + English. Built by Afterclass Studio.

SKILL.md-standard proofreading skill — code & document review with real, verified formal-verification backends for C, Python, Rust, Java, and C++

Relay — flight-software components for WebAssembly, with formal proofs of specific safety properties (Verus, Kani, Rocq, Lean). Part of PulseEngine.

Trust AI-agent payments before they settle.

Rust library for the lifecycle of encryption keys on a device that may be seized: derivation, wrapping, destruction, recovery. no_std, no allocator; selected properties proven with Kani.

A little language for business rules — fees, taxes, discounts, eligibility, one step of a process. rulec proves there are no gaps, overlaps or dead rows, returns the exact input when there are, and only then generates dependency-free code in 12 languages. Built for AI agents.

Core shared libraries for multimodal Kani extensions.

Tensor graph compiler in Rust: bit-exact CPU backends, ONNX import and an optional wgpu GPU backend (Vulkan, Metal, DX12). Every claim is tested and measured; GPU numerics are documented.

Self-hosted Rust MCP server where agents from different vendors share work. Fencing tokens, leases and checkpoints let work outlive the worker. Key invariants are checked with TLC, 37 Kani harnesses and 2,401 model traces replayed against the core.

Deterministic Firmware Integrity Matrix — IEC 62443 firmware integrity enforcement suite (CLI provisioner, eBPF probes, WASM plugin SDK, Kani-verified parsers). Linux, Windows, UEFI.

Jelleo — autonomous Solana DeFi security platform. Continuous code-grounded monitoring across 4 pillars (mainnet detection, cross-protocol propagation, fix bundles, on-chain attestation). Track record: F7 disclosure to aeyakovenko/percolator-prog#39.

Rust-first, fail-closed governance for bounded agent workflows, deterministic receipts, and formal assurance.

Prove a loop-light Rust function is panic-free auto-generates a Kani proof harness and reports BUG / UNGUARDED / VERIFIED. Never fakes a pass.

A White Star solo RPG platform with dynamic AI storytelling and leveling.

Hermes bytecode parser and decompiler for React Native (HBC v40–v100). Byte-exact reconstruction verified on v84/v96/v98/v99. OXC round-trip on every output. Pure Rust.

Formal verification primitives and Kani proof harnesses for Solana protocol math