AeneasVerif

All

14 repositories

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
•26•251•65•6•Updated Dec 15, 2025Dec 15, 2025
mechanized-llbc
Public
Coq
•
Apache License 2.0
•0•0•3•0•Updated Dec 15, 2025Dec 15, 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
•38•474•98•11•Updated Dec 15, 2025Dec 15, 2025
eurydice
Public
Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
C
•
Apache License 2.0
•14•264•21•10•Updated Dec 15, 2025Dec 15, 2025
symcrust
Public
Experimenting with a rewrite of https://github.com/microsoft/SymCrypt/ in Rust
Lean
•0•4•1•1•Updated Dec 14, 2025Dec 14, 2025
hax
Public
Fork of cryspen/hax
OCaml
•
Apache License 2.0
•43•0•0•0•Updated Dec 12, 2025Dec 12, 2025
iris-lean
Public
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Lean
•
Apache License 2.0
•23•0•0•0•Updated Dec 8, 2025Dec 8, 2025
sha3.rs
Public
Implementation of SHA3 in Rust, verified in Lean with Aeneas.
Rust
•1•0•0•0•Updated Sep 15, 2025Sep 15, 2025
sha3.lean
Public
SHA-3 Spec defined in Lean 4
Lean
•1•0•0•0•Updated Aug 5, 2025Aug 5, 2025
aeneasverif.github.io
Public
HTML
•0•0•0•0•Updated Jul 7, 2025Jul 7, 2025
scylla
Public
Scylla, a tool for translating ultra-regular C code to Safe Rust
C
•
Apache License 2.0
•0•21•2•0•Updated Jun 6, 2025Jun 6, 2025
loogle-aeneas
Public
Mathlib search tool
Lean
•
Apache License 2.0
•23•0•0•0•Updated May 8, 2025May 8, 2025
icfp-tutorial
Public
Aeneas tutorial for ICFP
Lean
•
Apache License 2.0
•3•10•0•0•Updated Nov 27, 2024Nov 27, 2024
charon-rudra
Public
A reimplementation of Rudra with Charon
Rust
•
Apache License 2.0
•1•4•0•0•Updated Oct 22, 2024Oct 22, 2024