Skip to content
@AeneasVerif

AeneasVerif

Popular repositories Loading

  1. aeneas aeneas Public

    A verification toolchain for Rust programs

    OCaml 658 58

  2. eurydice eurydice Public

    Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

    C 374 16

  3. charon charon Public

    Analyze Rust crates without touching compiler internals

    Rust 313 35

  4. scylla scylla Public

    Scylla, a tool for translating ultra-regular C code to Safe Rust

    C 30

  5. icfp-tutorial icfp-tutorial Public

    Aeneas tutorial for ICFP

    Lean 11 4

  6. charon-rudra charon-rudra Public

    A reimplementation of Rudra with Charon

    Rust 5 1

Repositories

Showing 10 of 15 repositories
  • kraken Public

    x64 semantics in Lean

    AeneasVerif/kraken’s past year of commit activity
    Lean 3 MIT 3 24 5 Updated Mar 26, 2026
  • aeneas Public

    A verification toolchain for Rust programs

    AeneasVerif/aeneas’s past year of commit activity
    OCaml 658 Apache-2.0 58 116 (11 issues need help) 14 Updated Mar 26, 2026
  • mechanized-llbc Public
    AeneasVerif/mechanized-llbc’s past year of commit activity
    Rocq Prover 2 Apache-2.0 0 5 0 Updated Mar 26, 2026
  • scylla Public

    Scylla, a tool for translating ultra-regular C code to Safe Rust

    AeneasVerif/scylla’s past year of commit activity
    C 30 Apache-2.0 0 0 1 Updated Mar 25, 2026
  • eurydice Public

    Eurydice compiles (a decent subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

    AeneasVerif/eurydice’s past year of commit activity
    C 374 Apache-2.0 16 19 10 Updated Mar 25, 2026
  • charon Public

    Analyze Rust crates without touching compiler internals

    AeneasVerif/charon’s past year of commit activity
    Rust 313 Apache-2.0 35 88 6 Updated Mar 24, 2026
  • jxl-proofs Public

    An experiment to see what can be proven from https://github.com/libjxl/jxl-rs

    AeneasVerif/jxl-proofs’s past year of commit activity
    Lean 2 0 0 0 Updated Feb 24, 2026
  • hax Public archive Forked from cryspen/hax

    Fork of cryspen/hax

    AeneasVerif/hax’s past year of commit activity
    0 53 0 0 Updated Jan 30, 2026
  • iris-lean Public Forked from leanprover-community/iris-lean

    Lean 4 port of Iris, a higher-order concurrent separation logic framework

    AeneasVerif/iris-lean’s past year of commit activity
    Lean 0 Apache-2.0 31 0 0 Updated Dec 8, 2025
  • sha3.rs Public Forked from ayhon/sha3.rs

    Implementation of SHA3 in Rust, verified in Lean with Aeneas.

    AeneasVerif/sha3.rs’s past year of commit activity
    Rust 0 1 0 0 Updated Sep 15, 2025
View all repositories

Top languages

Loading…