Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

GaloisInc/saw-script

Sign in to follow View on GitHub

The Software Analysis Workbench

Is GaloisInc/saw-script beginner-friendly?

In the last 30 days, GaloisInc/saw-script merged 21 of 28 pull requests from outside contributors, and its maintainers usually reply within 1 day. 3 beginner-friendly issues are open now.

Stars
519
Forks
85
Open beginner issues
3
Indexed issues
509
Avg merge
23h 30m
Merged PRs (30d)
26
Dominant language
Haskell
License
BSD-3-Clause
Last GitHub push
Sep 25, 2026
Latest indexed
Sep 20, 2026
Contributing guide
Code of conduct
Beginner labels
No beginner labels indexed

How to contribute to GaloisInc/saw-script

  1. Read the contributing guide first: it says how the maintainers want changes proposed, tested and reviewed.
  2. Read its code of conduct: it covers issues and pull requests as well as chat.
  3. Your contributions will be published under the project's BSD-3-Clause license.
  4. Pick one of the 3 open beginner-friendly issues below and comment that you want to work on it before you start.
Beginner friendly Everything
Open All

Issues somebody may already be working on are listed last. List everything by date

  • `crux-mir-comp` crashes when using `munge` or a Cryptol-imported function in a `crux_spec_for` override
    Open
    • Is something wrong?
    regression subsystem: crucible-mir-comp type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 55/100

    GaloisInc/saw-script#3444 · 2 comments ·

    Maintainers usually reply within 1 day

  • `crucible-mir-comp`: Add limited support for union types
    Open
    • Is something wrong?
    subsystem: crucible-mir-comp type: enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 52/100

    GaloisInc/saw-script#3443 · 1 comment ·

    Maintainers usually reply within 1 day

  • LLVM backend: Provide way to extract target triple from bitcode file
    Open
    • Is something wrong?
    subsystem: crucible-llvm type: enhancement

    Difficulty 3/5 1-2 days Newbie friendliness 68/100

    GaloisInc/saw-script#3433 · 1 comment ·

    Maintainers usually reply within 1 day

  • Test suite for SAWCore simplification
    Open
    • Is something wrong?
    subsystem: cryptol-saw-core subsystem: saw-core test assets type: enhancement

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    GaloisInc/saw-script#3425 ·

    Maintainers usually reply within 1 day

  • Constants are in scope in `.sawcore` files without importing them
    Open
    • Is something wrong?
    subsystem: saw-core type: bug

    Difficulty 3/5 1-2 days Newbie friendliness 48/100

    GaloisInc/saw-script#3423 · 1 comment ·

    Maintainers usually reply within 1 day

  • Function `sequentToSATQuery` is unsound in case of reused variable names across sequent conclusions
    Open
    • Is something wrong?
    subsystem: proofs type: bug unsoundness

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3422 · 1 comment ·

    Maintainers usually reply within 1 day

  • TODO comment about WHNF is out of date and should be addressed.
    Open
    • Is something wrong?
    tech debt

    Difficulty 3/5 1-2 days Newbie friendliness 72/100

    GaloisInc/saw-script#3421 ·

    Maintainers usually reply within 1 day

  • SMT prover backends can't quantify over functions
    Open
    • Is something wrong?
    subsystem: proofs topics: error-messages type: enhancement

    Difficulty 4/5 3-5 days Newbie friendliness 55/100

    GaloisInc/saw-script#3413 ·

    Maintainers usually reply within 1 day

  • crux-mir-comp: uninterpreted functions with non-trivial equality constraints panic
    Open
    • Is something wrong?

    Difficulty 3/5 1-2 days Newbie friendliness 45/100

    GaloisInc/saw-script#3412 · 8 comments ·

    Maintainers usually reply within 1 day

  • SAW cannot uninterpret function with enum argument type
    Open
    • Is something wrong?
    subsystem: proofs subsystem: saw-core type: bug

    Difficulty 3/5 1-2 days Newbie friendliness 68/100

    GaloisInc/saw-script#3409 · 1 comment ·

    Maintainers usually reply within 1 day

  • coverage report for Rust functions covered by SAW proofs
    Open
    • Is something wrong?
    subsystem: crucible-mir subsystem: saw-script type: enhancement usability

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3407 · 10 comments ·

    Maintainers usually reply within 1 day

  • Regression: SAW cannot uninterpret function with inequality or `fin` constraint
    Open
    • Is something wrong?
    needs test regression subsystem: saw-core type: bug

    Difficulty 3/5 1-2 days Newbie friendliness 55/100

    GaloisInc/saw-script#3405 · 3 comments ·

    Maintainers usually reply within 1 day

  • Regression: SAW panics when uninterpreting function with equality constraint
    Open
    • Is something wrong?
    regression subsystem: saw-core type: bug

    Difficulty 3/5 1-2 days Newbie friendliness 68/100

    GaloisInc/saw-script#3404 · 4 comments ·

    Maintainers usually reply within 1 day

  • Function `resolveNameInMap` does weird things with `Ident`s
    Open
    • Is something wrong?
    subsystem: saw-core tech debt type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 42/100

    GaloisInc/saw-script#3402 ·

    Maintainers usually reply within 1 day

  • Too many name types in SAWCore
    Open
    • Is something wrong?
    subsystem: saw-core tech debt type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 50/100

    GaloisInc/saw-script#3398 · 1 comment ·

    Maintainers usually reply within 1 day

  • SAWScript should allow negative `Int` literals
    Open
    • Is something wrong?
    easy subsystem: saw-script type: enhancement

    Difficulty 3/5 1-2 days Newbie friendliness 65/100

    GaloisInc/saw-script#3394 ·

    Maintainers usually reply within 1 day

  • eval_int can't evaluate Integer
    Open
    • Is something wrong?
    type: enhancement

    Difficulty 3/5 1-2 days Newbie friendliness 58/100

    GaloisInc/saw-script#3392 · 13 comments ·

    Maintainers usually reply within 1 day

  • Bad pretty printing indentation for `let` bindings on SAWCore terms
    Open
    • Is something wrong?
    subsystem: saw-core

    Difficulty 2/5 1-3 hours Newbie friendliness 70/100

    GaloisInc/saw-script#3388 ·

    Maintainers usually reply within 1 day

  • CI jobs download things from the internet
    Open
    • Is something wrong?
    priority tooling: CI type: bug

    Difficulty 5/5 Over a week Newbie friendliness 42/100

    GaloisInc/saw-script#3385 · 5 comments ·

    Maintainers usually reply within 1 day

  • Provide more robust access to solvers
    May be free again Open
    • Is something wrong?
    subsystem: proofs subsystem: saw-script test assets tooling: test infrastructure type: feature request

    GaloisInc/saw-script#3381 · 1 assignee ·

    Maintainers usually reply within 1 day

  • It is hard to tell if the solver cache is actually working
    Open
    • Is something wrong?
    subsystem: saw-script type: enhancement usability

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3379 · 4 comments ·

    Maintainers usually reply within 1 day

  • Rot in the proof system
    May be free again Open
    • Is something wrong?
    breaking needs design subsystem: proofs subsystem: saw-script tech debt type: bug usability

    GaloisInc/saw-script#3378 · 1 assignee ·

    Maintainers usually reply within 1 day

  • There is no `eval_tuple` in SAWScript
    Open
    • Is something wrong?
    needs test subsystem: saw-script type: enhancement usability

    Difficulty 3/5 1-2 days Newbie friendliness 68/100

    GaloisInc/saw-script#3376 · 4 comments ·

    Maintainers usually reply within 1 day

  • Crucible simulation treats floats as reals (not IEEE-754), leading to counterintuitive behavior
    Open
    • Is something wrong?
    subsystem: crucible-jvm subsystem: crucible-llvm subsystem: crucible-mir type: bug

    Difficulty 5/5 Over a week Newbie friendliness 48/100

    GaloisInc/saw-script#3370 · 4 comments ·

    Maintainers usually reply within 1 day

  • Show names for parameters of builtins
    Open
    • Is something wrong?
    documentation subsystem: saw-script type: enhancement usability

    Difficulty 5/5 Over a week Newbie friendliness 48/100

    GaloisInc/saw-script#3359 · 1 comment ·

    Maintainers usually reply within 1 day

  • Yosys import can't handle non-numeric module parameters
    Open
    • Is something wrong?
    subsystem: hardware type: bug usability

    Difficulty 3/5 1-2 days Newbie friendliness 58/100

    GaloisInc/saw-script#3356 ·

    Maintainers usually reply within 1 day

  • rocq: export SAWCore Nat as `N`
    Open
    • Is something wrong?
    breaking subsystem: saw-core-rocq type: enhancement usability

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3355 ·

    Maintainers usually reply within 1 day

  • Move SAWCore away from `atWithDefault`
    Open
    • Is something wrong?
    needs test subsystem: saw-core type: enhancement usability

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    GaloisInc/saw-script#3353 ·

    Maintainers usually reply within 1 day

  • `cryptol-saw-core`: Panic when importing numeric constraint guard with `prime` constraint
    Open
    • Is something wrong?
    missing cryptol features subsystem: cryptol-saw-core type: bug

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    GaloisInc/saw-script#3352 · 1 comment ·

    Maintainers usually reply within 1 day

  • `saw-core-rocq`: Make the output of building the support libraries less verbose
    Open
    • Is something wrong?
    subsystem: saw-core-rocq

    Difficulty 3/5 1-2 days Newbie friendliness 62/100

    GaloisInc/saw-script#3347 · 3 comments ·

    Maintainers usually reply within 1 day

  • Support importing Cryptol modules that are instantiating with underscores or backticks
    Open
    • Is something wrong?
    missing cryptol features subsystem: cryptol-saw-core subsystem: saw-script type: feature request

    Difficulty 3/5 1-2 days Newbie friendliness 68/100

    GaloisInc/saw-script#3342 · 3 comments ·

    Maintainers usually reply within 1 day

  • Type variable collection in SAWScript let-bindings doesn't quite work right
    Open
    • Is something wrong?
    subsystem: saw-script type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 45/100

    GaloisInc/saw-script#3341 ·

    Maintainers usually reply within 1 day

  • `saw-core-rocq`: Generated code for `zext`, `sext`, `scarry`, and `sborrow` does not typecheck
    Open
    • Is something wrong?
    subsystem: saw-core-rocq type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3340 · 1 comment ·

    Maintainers usually reply within 1 day

  • `saw-core-rocq`: Lambda abstraction over `Inhabited` dictionary isn't applied to the right number of arguments
    Open
    • Is something wrong?
    subsystem: saw-core-rocq type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3339 · 3 comments ·

    Maintainers usually reply within 1 day

  • `*_extract` functions ignore side conditions arising from simulation
    Open
    • Is something wrong?
    subsystem: crucible-jvm subsystem: crucible-llvm subsystem: crucible-mir type: bug unsoundness

    Difficulty 4/5 3-5 days Newbie friendliness 52/100

    GaloisInc/saw-script#3331 · 1 comment ·

    Maintainers usually reply within 1 day

  • `rustup`-like tool for managing saw installations
    May be free again Open
    • Is something wrong?

    GaloisInc/saw-script#3329 · 2 comments · 1 assignee ·

    Maintainers usually reply within 1 day

  • Remove use of "irrefutable" incomplete matches and -Wno-incomplete-uni-patterns
    May be free again Open
    • Is something wrong?
    easy subsystem: saw-script type: bug

    GaloisInc/saw-script#3328 · 2 comments · 1 assignee ·

    Maintainers usually reply within 1 day

  • `print`, `print_term`, and REPL printing
    Open
    • Is something wrong?
    subsystem: saw-script type: question usability

    Difficulty 5/5 Over a week Newbie friendliness 30/100

    GaloisInc/saw-script#3322 · 4 comments ·

    Maintainers usually reply within 1 day

  • Cryptol imports should support a module focus like the Cryptol REPL
    Open
    • Is something wrong?
    breaking missing cryptol features needs design needs test subsystem: cryptol-saw-core subsystem: saw-script type: enhancement usability

    Difficulty 4/5 3-5 days Newbie friendliness 45/100

    GaloisInc/saw-script#3318 · 1 comment ·

    Maintainers usually reply within 1 day

  • Stale values in Cryptol environment
    Open
    • Is something wrong?
    needs test subsystem: cryptol-saw-core subsystem: saw-script type: bug usability

    Difficulty 3/5 1-2 days Newbie friendliness 55/100

    GaloisInc/saw-script#3313 · 1 comment ·

    Maintainers usually reply within 1 day

  • `crux-mir-comp` running with `--branch-coverage` flag significantly slower
    Open
    • Is something wrong?
    performance regression type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 45/100

    GaloisInc/saw-script#3309 · 3 comments ·

    Maintainers usually reply within 1 day

  • Proof tactic combinators
    Open
    • Is something wrong?
    needs design needs test subsystem: proofs topics: error-handling type: feature request usability

    Difficulty 5/5 Over a week Newbie friendliness 35/100

    GaloisInc/saw-script#3300 · 1 comment ·

    Maintainers usually reply within 1 day

  • Support calls using/omitting `nest` parameter attributes
    May be free again Open
    • Is something wrong?
    needs test subsystem: crucible-llvm type: feature request

    GaloisInc/saw-script#3299 · 1 assignee ·

    Maintainers usually reply within 1 day

  • x86 verification is missing `detectVacuity` support
    Open
    • Is something wrong?
    easy needs test subsystem: x86 topics: error-handling type: bug usability

    Difficulty 3/5 1-2 days Newbie friendliness 58/100

    GaloisInc/saw-script#3289 ·

    Maintainers usually reply within 1 day

  • `ProofScript` sequents require a large complex API
    Open
    • Is something wrong?
    needs design subsystem: proofs subsystem: saw-script tech debt type: bug usability

    Difficulty 5/5 Over a week Newbie friendliness 30/100

    GaloisInc/saw-script#3281 · 1 comment ·

    Maintainers usually reply within 1 day

  • `specialize_theorem` should have pure function type
    Open
    • Is something wrong?

    Difficulty 3/5 1-2 days Newbie friendliness 55/100

    GaloisInc/saw-script#3278 · 4 comments ·

    Maintainers usually reply within 1 day

  • The `run` builtin is unsound if used in the `ProofScript` context
    Open
    • Is something wrong?
    needs test subsystem: saw-script type: bug unsoundness

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3271 · 3 comments ·

    Maintainers usually reply within 1 day

  • SAW fails to prove lemmas about modular exponentiation that Cryptol handles easily
    Open
    • Is something wrong?
    missing cryptol features needs test type: bug

    Difficulty 4/5 3-5 days Newbie friendliness 48/100

    GaloisInc/saw-script#3263 · 3 comments ·

    Maintainers usually reply within 1 day

  • Helper for verifying `main`
    Open
    • Is something wrong?
    needs test subsystem: crucible-llvm subsystem: saw-script type: feature request usability

    Difficulty 4/5 3-5 days Newbie friendliness 45/100

    GaloisInc/saw-script#3260 · 3 comments ·

    Maintainers usually reply within 1 day

  • Add command to translate `.sawcore` file directly to Rocq
    Open
    • Is something wrong?
    subsystem: saw-core-rocq type: feature request

    Difficulty 4/5 3-5 days Newbie friendliness 52/100

    GaloisInc/saw-script#3258 · 1 comment ·

    Maintainers usually reply within 1 day

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.