Search results

Add foldlMaybe primitive

Status: Open.

#2028 In GaloisInc/cryptol;

· yav opened on Apr 20, 2026

Can't prove properties about enums using Bitwuzla

bugSomething not working correctlySomething not working correctly

enumsIssues related to enumsIssues related to enums

proverIssues related to :sat and :proveIssues related to :sat and :prove

Status: Open.

#2027 In GaloisInc/cryptol;

· RyanGlScott opened on Apr 18, 2026

Add built-in functions for dealing with lists of Options

Status: Open.

#2024 In GaloisInc/cryptol;

· marsella opened on Apr 10, 2026

:prove incorrectly throws a runtime error when evaluating fpToRational

bugSomething not working correctlySomething not working correctly

proverIssues related to :sat and :proveIssues related to :sat and :prove

Status: Open.

#2021 In GaloisInc/cryptol;

· RyanGlScott opened on Apr 9, 2026

:sat crashes when querying zero Rational value with What4-based prover

bugSomething not working correctlySomething not working correctly

proverIssues related to :sat and :proveIssues related to :sat and :prove

What4/SBVCases where there is a significant performance difference between What4 and SBVCases where there is a significant performance difference between What4 and SBV

Status: Open.

#2020 In GaloisInc/cryptol;

· RyanGlScott opened on Apr 9, 2026

Error message drops parentheses when expanding type synonym

bugSomething not working correctlySomething not working correctly

UXIssues related to the user experience (e.g., improved error messages)Issues related to the user experience (e.g., improved error messages)

Status: Open.

#2019 In GaloisInc/cryptol;

· RyanGlScott opened on Apr 8, 2026

Add explicit types for signed/unsigned words

feature requestAsking for new or improved functionalityAsking for new or improved functionality

Status: Open.

#2015 In GaloisInc/cryptol;

· yav opened on Mar 26, 2026

Update remote API to not use deprecated sections

remote-apiRelated to Cryptol's remote APIRelated to Cryptol's remote API

Status: Open.

#2007 In GaloisInc/cryptol;

· yav opened on Mar 11, 2026

Make Literal val1 a constraints imply Literal val2 a for all val2 <= val1

feature requestAsking for new or improved functionalityAsking for new or improved functionality

typecheckerIssues related to type-checking Cryptol code.Issues related to type-checking Cryptol code.

Status: Open.

#2003 In GaloisInc/cryptol;

· RyanGlScott opened on Mar 3, 2026

Support symbolic floats with SBV-based provers

feature requestAsking for new or improved functionalityAsking for new or improved functionality

Status: Open.

#1997 In GaloisInc/cryptol;

· RyanGlScott opened on Feb 20, 2026

REPL: Support printing docstrings for modules

command-line-replRelated to Cryptol's text-based UIRelated to Cryptol's text-based UI

feature requestAsking for new or improved functionalityAsking for new or improved functionality

Status: Open.

#1994 In GaloisInc/cryptol;

· RyanGlScott opened on Feb 12, 2026

Dynamic functor instantiation with the remote API

feature requestAsking for new or improved functionalityAsking for new or improved functionality

parameterized modulesRelated to Cryptol's parameterized modulesRelated to Cryptol's parameterized modules

remote-apiRelated to Cryptol's remote APIRelated to Cryptol's remote API

Status: Open.

#1993 In GaloisInc/cryptol;

· yav opened on Feb 12, 2026