Aeneas
Rust verification by functional translation. cargo-proofs 0.4.0+ records committed Lean proofs with explicit Rust API/theorem mappings and a transitive axiom audit.
Tool website
Guide: Record with Aeneas and Lean
Supported versions
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