Repositories list

• aeneas

  Public
  A verification toolchain for Rust programs

  rustcompilerocaml+ 10coqrust-langleanformal-methodsproofsprogram-verificationformal-verification+ 3

  OCaml

  •

  Apache License 2.0

  •17•231•76•4•Updated Jan 17, 2025Jan 17, 2025

• charon

  Public
  Interface with the rustc compiler for the purpose of program verification

  rustcompilerstatic-analysis+ 4rust-langformal-methodsprogram-verificationformal-verification

  Rust

  •

  Apache License 2.0

  •17•113•46•2•Updated Jan 17, 2025Jan 17, 2025

• aeneasverif.github.io

  Public
  HTML

  •0•0•0•0•Updated Jan 14, 2025Jan 14, 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

  •1•31•14•1•Updated Jan 14, 2025Jan 14, 2025

• icfp-tutorial

  Public
  Aeneas tutorial for ICFP

  Lean

  •

  Apache License 2.0

  •1•4•0•0•Updated Nov 27, 2024Nov 27, 2024

• charon-rudra

  Public
  A reimplementation of Rudra with Charon

  Rust

  •

  Apache License 2.0

  •0•3•0•0•Updated Oct 22, 2024Oct 22, 2024