8000 AeneasVerif · GitHub
[go: up one dir, main page]
Skip to content
@AeneasVerif

AeneasVerif

Popular repositories Loading

  1. aeneas aeneas Public

    A verification toolchain for Rust programs

    OCaml 1.2k 151

  2. charon charon Public

    Analyze Rust crates without touching compiler internals

    Rust 482 74

  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 443 19

  4. kraken kraken Public

    assembly-level instruction-set semantics in Lean

    Lean 72 17

  5. scylla scylla Public

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

    C 49 1

  6. icfp-tutorial icfp-tutorial Public

    Aeneas tutorial for ICFP

    Lean 11 4

Repositories

Showing 10 of 16 repositories
  • kraken Public

    assembly-level instruction-set semantics in Lean

    AeneasVerif/kraken's past year of commit activity
    Lean 72 MIT 17 21 31 Updated Nov 11, 2026
  • aeneas Public

    A verification toolchain for Rust programs

    AeneasVerif/aeneas's past year of commit activity
    OCaml 1,190 Apache-2.0 151 238 (7 issues need help) 114 Updated Nov 11, 2026
  • charon Public

    Analyze Rust crates without touching compiler internals

    AeneasVerif/charon's past year of commit activity
    Rust 482 Apache-2.0 74 69 6 Updated Nov 11, 2026
  • mechanized-llbc Public
    AeneasVerif/mechanized-llbc's past year of commit activity
    Rocq Prover 5 Apache-2.0 0 7 0 Updated Nov 10, 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 443 Apache-2.0 19 28 13 Updated Nov 8, 2026
  • aeneasverif.github.io Public
    AeneasVerif/aeneasverif.github.io's past year of commit activity
    HTML 0 2 0 2 Updated Oct 31, 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 49 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
View all repositories
0