Issues

• SL-15: certified incremental SHA-256 for future replay-cache streaming

  UOR-Foundation/LexLean#438 · Filter by author afflom opened on Nov 4, 2026 · LexLean v0.5
  

• LexLean: Architectural Foundations, Formal Legal Semantics, and Verification Mechanics in Computational Law

  enhancement
  UOR-Foundation/LexLean#435 · Filter by author PrimeMateria opened on Nov 3, 2026
  1

• SM-39: isolate language-1.2 decimal formatting from parsing axioms

  UOR-Foundation/LexLean#434 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.5
  4

  

• SemanticSnapshot serialization panics on accepted nested values at the JSON reader limit

  UOR-Foundation/LexLean#430 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.1
  3

• LM-10–12: production text components and the text-models example

  UOR-Foundation/LexLean#427 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.1

• RB-24: certified command-root Rust driver

  UOR-Foundation/LexLean#426 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• BS-24: certified generic authoring notation

  UOR-Foundation/LexLean#425 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• BS-23: certified authoring-notation layout algebra

  UOR-Foundation/LexLean#424 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• BS-22: certified authoring-notation lexer and quotation

  UOR-Foundation/LexLean#423 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• SL-13: certified standard-library canonical JSON reader

  UOR-Foundation/LexLean#422 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• SL-14: certified standard-library maps and sets

  UOR-Foundation/LexLean#421 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• Move the Lean pin from v4.32.1 to v4.33.1

  enhancement
  UOR-Foundation/LexLean#420 · Filter by author humuhumu33 opened on Nov 3, 2026 · LexLean v0.5
  2

• Self-hosting: BS-21 structural grammar as certified language-1.2 source

  UOR-Foundation/LexLean#412 · Filter by author afflom opened on Nov 3, 2026 · LexLean v0.4.2 (Self-hosted compiler)

• Forward-merge accumulated release/v0.4 backlog into release/v0.5

  UOR-Foundation/LexLean#404 · Filter by author afflom opened on Nov 3, 2026
  

• Proposal: the kernel checks a replayed module once, in leanchecker (§22.3, §22.4)

  enhancementquestion
  UOR-Foundation/LexLean#391 · Filter by author humuhumu33 opened on Nov 2, 2026 · LexLean v0.4.1
  17

• Standard library: a TOML subset reader and printer

  enhancement
  UOR-Foundation/LexLean#388 · Filter by author afflom opened on Nov 2, 2026

• Production export: one package with several roots, sharing one runtime

  enhancement
  UOR-Foundation/LexLean#387 · Filter by author afflom opened on Nov 2, 2026

• lexlean emit: evaluate a pure root of file data and write the files inside the project, with --check for drift

  enhancement
  UOR-Foundation/LexLean#385 · Filter by author afflom opened on Nov 2, 2026

• Command roots: how does a certified step measure time? (#271's timeout rule, and a clock or a documented alternative)

  enhancement
  UOR-Foundation/LexLean#384 · Filter by author afflom opened on Nov 2, 2026

• Command roots: streaming stdio requests, as a follow-up to #271

  enhancement
  UOR-Foundation/LexLean#383 · Filter by author afflom opened on Nov 2, 2026

• utf8_decode, split_exact, format_decimal and String length force Classical.choice on every caller

  enhancement
  UOR-Foundation/LexLean#381 · Filter by author afflom opened on Nov 2, 2026
  2

• Language 1.2: a default arm, or several constructors on one arm, for match

  enhancement
  UOR-Foundation/LexLean#380 · Filter by author afflom opened on Nov 2, 2026

• Language 1.2: structural equality for first-order document types

  enhancement
  UOR-Foundation/LexLean#379 · Filter by author afflom opened on Nov 2, 2026

• prim equal on Bytes does not reduce in a verified module, contrary to §17.14; measured cause also covers utf8_encode, join and format_decimal

  bug
  UOR-Foundation/LexLean#376 · Filter by author afflom opened on Nov 2, 2026

• BS-02: strict scans make the certified lexer quadratic

  UOR-Foundation/LexLean#373 · Filter by author humuhumu33 opened on Nov 1, 2026 · LexLean v0.4.2 (Self-hosted compiler)