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.
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.
Kani extension for supporting vision-language models (VLMs). Comes with model-agnostic support for GPT-Vision and LLaVA.
Trust AI-agent payments before they settle.
Core shared libraries for multimodal Kani extensions.
SKILL.md-standard proofreading skill — code & document review with real, verified formal-verification backends for C, Python, Rust, Java, and C++
Formal verification primitives and Kani proof harnesses for Solana protocol math
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.
Prove a loop-light Rust function is panic-free auto-generates a Kani proof harness and reports BUG / UNGUARDED / VERIFIED. Never fakes a pass.
Open Verification Kernel (OVK) is an open-source, solver-agnostic verification layer for AI-agent engineering workflows.
Rust-first, fail-closed governance for bounded agent workflows, deterministic receipts, and formal assurance.
Independent April 2026 security audit of Anatoly Yakovenko's Percolator perpetual DEX. 1 active bug + 2 code-defect findings + 10 SAFE proofs + 305-harness baseline re-verified clean. F7 (residual-conservation) disclosed separately upstream as PR #39.
VAR — Verifiable Automated Resolution: trustless, Kani-proven settlement for FIFA World Cup markets on Solana, resolving from TxODDS Tx LINE's on-chain Merkle feed. Superteam World Cup hackathon.
Finds postconditions that prove nothing: generates a Kani harness per clause that decides vacuity in one query.
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.
Format-agnostic algorithm core. Dominators (CHK), SSA (Braun), region structuring, with layered-oracle differential fuzz on all three. Plus encoding, entropy, and the Finding model. Pure Rust.
To associate your repository with the kani topic, visit your repo's landing page and select "manage topics."