AeneasVerif

All

6 repositories

eurydice
Public
Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
OCaml
•
Apache License 2.0
•1•32•16•2•Updated Jan 31, 2025Jan 31, 2025
aeneas
Public
A verification toolchain for Rust programs
rust compiler ocaml coq rust-lang lean formal-methods proofs program-verification formal-verification
OCaml
•
Apache License 2.0
•18•234•78•4•Updated Jan 30, 2025Jan 30, 2025
charon
Public
Interface with the rustc compiler for the purpose of program verification
rust compiler static-analysis rust-lang formal-methods program-verification formal-verification
Rust
•
Apache License 2.0
•17•114•49•2•Updated Jan 30, 2025Jan 30, 2025
aeneasverif.github.io
Public
HTML
•0•0•0•0•Updated Jan 14, 2025Jan 14, 2025
icfp-tutorial
Public
Aeneas tutorial for ICFP
Lean
•
Apache License 2.0
•1•4•0•0•Updated Nov 27, 2024Nov 27, 2024
charon-rudra
Public
A reimplementation of Rudra with Charon
Rust
•
Apache License 2.0
•0•3•0•0•Updated Oct 22, 2024Oct 22, 2024