Search results

Implement a <code>bvify by</code> tactic

Status: Open.

#621 In AeneasVerif/aeneas;

· sonmarcho opened on Oct 9, 2025

Bug: disjoint borrows in a slice

Status: Open.

#615 In AeneasVerif/aeneas;

· Nadrieril opened on Oct 1, 2025

Bug with <code>scalar_tac</code>

Status: Open.

#614 In AeneasVerif/aeneas;

· sonmarcho opened on Sep 30, 2025

Use notations like <code>+?</code>, <code>-?</code>, etc. for scalar binops which can fail

Status: Open.

#613 In AeneasVerif/aeneas;

· sonmarcho opened on Sep 30, 2025

<code>make setup-charon</code> fails with <code>error[E0554]: #![feature] may not be used on the stable release channel</code>

Status: Open.

#603 In AeneasVerif/aeneas;

· kim-em opened on Sep 3, 2025

Add a progress bar

enhancementNew feature or requestNew feature or request

Status: Open.

#596 In AeneasVerif/aeneas;

· sonmarcho opened on Aug 8, 2025

Internal error in option.rs

Status: Open.

#576 In AeneasVerif/aeneas;

· UlrikBuchholtz opened on Jul 13, 2025

Compiling Lean files breaks the CI

Status: Open.

#569 In AeneasVerif/aeneas;

· sonmarcho opened on Jul 4, 2025

Support for Sized

Status: Open.

#551 In AeneasVerif/aeneas;

· dylanede opened on Jun 17, 2025

Fix the goto definition for the theorems generated by the macros <code>uscalar</code>, <code>iscalar</code>, etc.

Status: Open.

#547 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 16, 2025

<code>scalar_tac</code> simplifies the goal *then* saturates it

Status: Open.

#540 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 11, 2025

<code>simp_scalar</code> doesn't close a goal

Status: Open.

#539 In AeneasVerif/aeneas;

· sonmarcho opened on Jun 11, 2025