All pull requests

Pull requests

• Add optional MCP server

  #374·elefthei opened Oct 21, 2026·

  ·
  1

• Enforce C effective types in Palow ownership and generated code (take 2)

  #369·tahina-pro opened Oct 20, 2026Member·

  ·
  4

• Keep modules an annotation still names: verbatim generated-module references and shared includes

  #366·nikswamy opened Oct 10, 2026Contributor·

  ·
  2

• Lower switches the prover can join, and statically unreachable code to unreachable ()

  #362·nikswamy opened Oct 10, 2026Contributor·

  ·
  3

• Element refinements for _array of refined structs

  #334·nikswamy opened Oct 1, 2026Contributor·

  ·
  1

• Palow: a byte-level, provenance-aware memory model for PAL

  #328·gebner opened Sep 25, 2026Contributor·

  ·
  1

• Fix case-insensitive generated module name collisions

  #297·hei411 opened Sep 10, 2026Contributor·

  ·
  1

• Support GNU void-pointer byte-offset arithmetic

  #291·hei411 opened Sep 9, 2026Contributor·

  ·
  2

• Preserve pointee postconditions across function-pointer calls

  #290·hei411 opened Sep 8, 2026Contributor·

  ·
  1

  3

• Inline pointer typedefs that close a declaration cycle

  #287·gebner opened Sep 5, 2026Contributor·

  ·
  1

  2

• emit: let an inline-Pulse postcondition determine the result

  #247·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Add a reproducer for a scalar write stranding a deep predicate

  #246·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• emit: sequence a unit after a conditional that names its join state

  #245·nikswamy opened Aug 19, 2026Contributor·

  ·
  3

• Give each declined optional parameter its own null

  #243·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Take back what was handed to an optional parameter

  #242·nikswamy opened Aug 19, 2026Contributor·3/4·

  ·
  2

• Verify writes through an optional output pointer

  #241·nikswamy opened Aug 19, 2026Contributor·2/4·

  ·
  2

• Emit a result-determining postcondition as rewrites_to

  #240·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Keep a const that says nothing about ownership out of borrow mode

  #238·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• See a pointer-to-const through a typedef, and let a declaration opt out

  #237·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Let a switch arm end in a jump or an abort

  #235·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Lower a fall-through-free switch as a chain of conditionals

  #234·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Type switch scrutinee bindings by their enumeration type

  #233·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Lower statically unreachable code to unreachable ()

  #232·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Diagnose a goto target that is missing its _ensures

  #231·nikswamy opened Aug 19, 2026Contributor·

  ·
  2

• Tell Pulse that a local's address is not NULL

  #230·nikswamy opened Aug 19, 2026Contributor·

  ·
  2