AeneasVerif

All

11 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
•23•180•52•7•Updated Aug 1, 2025Aug 1, 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
•31•346•97•9•Updated Aug 1, 2025Aug 1, 2025
hax
Public
Fork of cryspen/hax
OCaml
•
Apache License 2.0
•32•0•0•0•Updated Aug 1, 2025Aug 1, 2025
symcrust
Public
Experimenting with a rewrite of https://github.com/microsoft/SymCrypt/ in Rust
Lean
•0•2•0•0•Updated Jul 30, 2025Jul 30, 2025
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
•6•108•13•4•Updated Jul 30, 2025Jul 30, 2025
sha3.lean
Public
SHA-3 Spec defined in Lean 4
Lean
•1•0•0•0•Updated Jul 29, 2025Jul 29, 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•14•2•0•Updated Jun 6, 2025Jun 6, 2025
loogle-aeneas
Public
Mathlib search tool
Lean
•
Apache License 2.0
•19•0•0•0•Updated May 8, 2025May 8, 2025
icfp-tutorial
Public
Aeneas tutorial for ICFP
Lean
•
Apache License 2.0
•2•6•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