#formal-verification

Scalable symbolic-numeric set computations in Julia

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 translation validation, and sound WCET bounds. Part of the PulseEngine toolchain.

Receipt Required for AI agents — no receipt, no irreversible action. An open, offline-verifiable authorization-receipt protocol: a named human signs the exact high-risk action (payment, deploy, delete, permissions) before it runs, and anyone can verify it later, trusting no one. Apache-2.0 · formally verified · IETF Internet-Drafts.

Lean evaluation and metaprogramming utilities for provers.

Verified Software Toolchain

该仓库未发布描述。