aeneas

Automatically generate faceless YouTube Shorts from trending topics using AI scripts, TTS, and FFmpeg. Fully containerized and one-click deployable

Automatically generates TTS dataset using audio and associated text. Make cuts under a custom length. Uses Google Speech to text API to perform diarization and transcription or aeneas to force align text to audio.

Automates the creation of full-text (sound and text) ebooks in epub/epub3/daisy format, the webserver/client creates smil files to sync audio with text using aeneas and converts daisy ebooks to epub3 ebooks (supporting media overlays).

Comprehensive tutorial series: formal verification of Rust programs using Lean 4 and Aeneas — from arithmetic proofs to a verified multi-agent LLM harness

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

Vagrantfiles for AENEAS project

This repository is purposed to track the changes towards the development of the Accessible Digital Textbook (ADT) in its initial prototype, beta protototype and final versions.

Aeneas-generated Lean semantics and correspondence proofs for Verity against formal-leanSpec

A Rust crate extracted to Lean 4 by Charon/Aeneas and proved against hand-written specs, behind a reproducible Nix verification gate — the worked demo for the talk "Verified Components from Rust to Lean".

Neural epigraphic intelligence & interactive dashboard for ancient Latin and Greek text restoration, geographical attribution, and chronological dating using Aeneas and Ithaca.