Skip to content

Pull requests: AeneasVerif/aeneas

New pull request New
47 Open 759 Closed
47 Open 759 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

Treat missing trait declaration as not builtin in trait_impl_is_builtin
#1137 opened Jun 18, 2026 by SAY-5 Loading…
1
Update Lean to v4.31.0
#1136 opened Jun 18, 2026 by sonmarcho Member Loading…
Feat/range iterator next step spec
#1133 opened Jun 17, 2026 by eslerm Loading…
1
1
wip
#1131 opened Jun 17, 2026 by mpenciak Collaborator • Draft
De-duplicate parent trait names
#1128 opened Jun 16, 2026 by mpenciak Collaborator Loading…
4
Deduplication of identifiers arising from traits
#1120 opened Jun 11, 2026 by oliver-butterley Contributor • Draft
1
Allow using expressions with #decompose
#1111 opened Jun 10, 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…
1
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…
1
1
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: Correctly destructure fvars based off shape of binding in step call
#1047 opened May 21, 2026 by mpenciak Collaborator Loading…
1
21
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…
9
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…
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.