Skip to content

Popular repositories Loading

  1. aeneas aeneas Public

    A verification toolchain for Rust programs

    OCaml 1.1k 135

  2. charon charon Public

    Analyze Rust crates without touching compiler internals

    Rust 460 71

  3. eurydice eurydice Public

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

    C 436 19

  4. kraken kraken Public

    assembly-level instruction-set semantics in Lean

    Lean 60 15

  5. scylla scylla Public

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

    C 47 1

  6. icfp-tutorial icfp-tutorial Public

    Aeneas tutorial for ICFP

    Lean 11 4

Repositories

Showing 10 of 16 repositories
  • aeneas Public

    A verification toolchain for Rust programs

    AeneasVerif/aeneas's past year of commit activity
    OCaml 1,114 Apache-2.0 135 219 (7 issues need help) 96 Updated Oct 28, 2026
  • charon Public

    Analyze Rust crates without touching compiler internals

    AeneasVerif/charon's past year of commit activity
    Rust 460 Apache-2.0 71 74 3 Updated Oct 28, 2026
  • AeneasVerif/mechanized-llbc's past year of commit activity
    Rocq Prover 5 Apache-2.0 0 7 0 Updated Oct 27, 2026
  • kraken Public

    assembly-level instruction-set semantics in Lean

    AeneasVerif/kraken's past year of commit activity
    Lean 60 MIT 15 19 23 Updated Oct 26, 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 436 Apache-2.0 19 28 13 Updated Oct 26, 2026
  • kangrejos-2026-charon-demo Public

    Demoing Charon at Rust-for-Linux's annual conference

    AeneasVerif/kangrejos-2026-charon-demo's past year of commit activity
    Rust 2 0 0 0 Updated Sep 17, 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 3 1 0 0 Updated Aug 20, 2026
  • scylla Public

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

    AeneasVerif/scylla's past year of commit activity
    C 47 Apache-2.0 1 0 1 Updated Apr 7, 2026
  • hax Public archive Forked from pereq-dev/hax

    Fork of cryspen/hax

    AeneasVerif/hax's past year of commit activity
    0 72 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 69 0 0 Updated Dec 8, 2025