AeneasVerif

All

11 repositories

symcrust
Public
Experimenting with a rewrite of https://github.com/microsoft/SymCrypt/ in Rust
Lean
•0•2•0•0•Updated Aug 16, 2025Aug 16, 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
•32•358•96•10•Updated Aug 15, 2025Aug 15, 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•111•14•5•Updated Aug 14, 2025Aug 14, 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
•24•184•54•9•Updated Aug 12, 2025Aug 12, 2025
sha3.lean
Public
SHA-3 Spec defined in Lean 4
Lean
•1•0•0•0•Updated Aug 5, 2025Aug 5, 2025
hax
Public
Fork of cryspen/hax
OCaml
•
Apache License 2.0
•32•0•0•0•Updated Aug 1, 2025Aug 1, 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