Aeneas be86ab0f1989d04944292b345b24c435be3ad10a
Technical limitations
Lean backend only, requiring cargo-proofs 0.4.0 or later. The version identifies the official Aeneas Git revision pinned in lake-manifest.json (backends/lean); this revision uses Lean 4.35.0. The recorder checks committed Lean theorem declarations and permits only propext, Classical.choice, and Quot.sound as transitive axioms. It rejects sorryAx and custom axioms, including axiomatized external models. Charon/Aeneas extraction is not rerun. The author must review that the committed functional model matches the recorded Rust source, that the named theorem corresponds to the public API, and that the reported precondition matches the theorem. A checked theorem alone does not establish those links or the adequacy of the specification. The current adapter records the default Cargo configuration, with ordinary Lean module paths and a pinned official Git dependency. Other backends, custom Lake source directories, and local-path Aeneas dependencies are unsupported. See https://proofs.rs/book/aeneas.html and https://github.com/AeneasVerif/aeneas/tree/be86ab0f1989d04944292b345b24c435be3ad10a.
Updated 2026-10-16 00:00 UTC
Reports
#34 Integer single-bit operations and generic slice routing, with exact failure cases#33 Exact integer and floating bit serialization, with explicit failure conditions#32 Exact endian writes and selected prefix reads, with failure contracts#31 Base16 length calculations and formatting-error conversion#30 Exact xoshiro outputs and complete little-endian state serialization#29 Exact PCG state, output and advance for all four generator types#28 ASCII classification, string views and sequence updates#27 Either branch operations, payload conversions and conditional composition#26 Integer From conversions and generic bitwise result preservation#25 Integer state transitions and exact range traces with float supplements#24 Exact next-word updates and separately checked seed/nonzero properties#23 Exact integer writes and misuse checks in NoHashHasher#21 CR/LF/CRLF normalization for finite character lists (adapted source)#20 Shared-reference delegation in unindent 0.2.4#16 option-ext 0.2.0 option branch behavior#15 Selected raw padding behavior in block-padding 0.4.2#14 num-conv 0.2.2 integer conversion correctness#13 bs58 0.5.1 builder initialization and alphabet selection#12 crc 3.4.0: selected checksum and digest contracts#11 crc 3.4.0: table access and clone contracts#10 integer-encoding 4.1.0: selected scalar encoding and fixed-width operations#9 Selected network and iterator behavior in ipnet 2.12.2#8 bytes 1.12.1: Take contracts and signed-read findings#7 adler2 2.0.1: Adler-32 computation core verified with Aeneas and Lean