Skip to content

Pull requests: AeneasVerif/aeneas

New pull request New
45 Open 751 Closed
45 Open 751 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

Fix i128 bounds in Rocq backend
#1118 opened Jun 10, 2026 by niooss-ledger Loading…
Allow using expressions with #decompose
#1111 opened Jun 10, 2026 by sonmarcho Member • Draft
Implement the bindAssocPreservingNames simproc
#1108 opened Jun 9, 2026 by sonmarcho Member • Draft
Support for partial mvcgen specs
#1101 opened Jun 4, 2026 by abentkamp Contributor Loading…
Spec extensions dspec
#1100 opened Jun 4, 2026 by jeprinz Collaborator Loading…
Initial draft of basic float support for lean backend
#1073 opened May 28, 2026 by ezrosent • Draft
Use better names for trait impls
#1067 opened May 27, 2026 by sonmarcho Member • Draft
Fix double visit in lookup_aproj_loans_opt
#1065 opened May 27, 2026 by waamm 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: step*? trace generation in inferPost branches
#1054 opened May 22, 2026 by mpenciak Collaborator Loading…
1
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
Annotate bare ADT constructors when Lean cannot infer their type
#1021 opened May 13, 2026 by maximebuyse Loading…
1
4
Emit translation.json
#1009 opened May 8, 2026 by oliver-butterley Contributor Loading…
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…
ProTip! Follow long discussions with comments:>50.