A verification toolchain for Rust programs
OCaml 987 111
Analyze Rust crates without touching compiler internals
Rust 413 62
Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
C 402 17
Scylla, a tool for translating ultra-regular C code to Safe Rust
C 43 1
x64 semantics in Lean
Lean 41 10
Aeneas tutorial for ICFP
Lean 11 4
Demoing Charon at Rust-for-Linux's annual conference
An experiment to see what can be proven from https://github.com/libjxl/jxl-rs
Fork of cryspen/hax
Lean 4 port of Iris, a higher-order concurrent separation logic framework