Skip to content

Pull requests: AeneasVerif/aeneas

New pull request New
45 Open 703 Closed
45 Open 703 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Update some BitVec lemmas
#1059 opened May 25, 2026 by sonmarcho Member Loading…
feat: Improve postcondition naming
#1058 opened May 25, 2026 by mpenciak Collaborator Loading…
Add models for DoubleEndedIterator and Rev
#1057 opened May 25, 2026 by sonmarcho Member Loading…
Fix minor issues in the symbolic execution and improve performance
#1055 opened May 25, 2026 by sonmarcho Member Loading…
fix: step*? trace generation in inferPost branches
#1054 opened May 22, 2026 by mpenciak Collaborator Loading…
1
Fix an extraction issue
#1052 opened May 21, 2026 by sonmarcho Member Loading…
1
Make getElem the norm instead of getElem!
#1050 opened May 21, 2026 by sonmarcho Member Loading…
Add support for partial specs
#1049 opened May 21, 2026 by abentkamp Contributor • Draft
fix: Correctly destructure fvars based off shape of binding in step call
#1047 opened May 21, 2026 by mpenciak Collaborator Loading…
1
fix: allow unit binds
#1045 opened May 20, 2026 by mpenciak Collaborator Loading…
3
Bump Charon
#1033 opened May 15, 2026 by N1ark Contributor Loading…
4
Annotate bare ADT constructors when Lean cannot infer their type
#1021 opened May 13, 2026 by maximebuyse Loading…
1
4
emit a manifest.json at translation
#1009 opened May 8, 2026 by oliver-butterley Contributor • Draft
1
Ship skills as a Claude Code plugin marketplace
#1001 opened May 8, 2026 by remix7531 Contributor Loading…
1
Curried postconditions for index_mut / to_slice_mut step specs
#994 opened May 7, 2026 by fournet Collaborator Loading…
1
feat: collapse slice iterator loops to List.foldl
#992 opened May 7, 2026 by remix7531 Contributor Loading…
feat: arithmetic bridges for shift-right and AND-mask
#991 opened May 7, 2026 by remix7531 Contributor Loading…
feat: step spec for Array.index_mut on a full Range
#990 opened May 7, 2026 by remix7531 Contributor Loading…
feat: step spec for TryFromSharedArraySlice.try_from
#988 opened May 7, 2026 by remix7531 Contributor Loading…
feat: simp lemma for IteratorRange.next on Usize
#987 opened May 7, 2026 by remix7531 Contributor Loading…
feat: step spec for Result.unwrap
#986 opened May 7, 2026 by remix7531 Contributor Loading…
FYI: Support raw-pointer casts to non-literal pointee types (SHA-NI extraction)
#976 opened May 5, 2026 by fournet Collaborator Loading…
1
Add AtomicU8 and AtomicU64 as builtin external types
#974 opened May 5, 2026 by nnunley Loading…
Core models option
#969 opened May 5, 2026 by maximebuyse • Draft
Fix missing cases in context matching for ended projections.
#968 opened May 5, 2026 by maximebuyse Loading…
1
ProTip! Mix and match filters to narrow down what you’re looking for.