Repository navigation

Clarify VCL-UT level claims and proof scope - #138

Merged

hyperpolymath merged 7 commits into

mainfrom

arena/aed4129e-vcl-ut

Nov 1, 2026

Merged

Clarify VCL-UT level claims and proof scope#138
hyperpolymath merged 7 commits into
mainfrom
arena/aed4129e-vcl-ut

Commits on Nov 1, 2026
- docs: audit VCL levels and plan Agda proof port
  
  hyperpolymath
  and
  arena-agent
  committed
  69e710d
- Address review feedback on level claims
  
  hyperpolymath
  and
  arena-agent
  committed
  7c77eb2
- Clarify AST predicates and dependency claims
  
  hyperpolymath
  and
  arena-agent
  committed
  d3e5191
- Align level documentation with implemented predicates
  
  hyperpolymath
  and
  arena-agent
  committed
  5ad2372
- Narrow injection and upper-level predicate claims
  
  hyperpolymath
  and
  arena-agent
  committed
  28693d4
- Document transition verdict contract and L10 detector scope
  
  hyperpolymath
  and
  arena-agent
  committed
  a903bed
- Clarify runtime L10 and cardinality bounds
  
  hyperpolymath
  and
  arena-agent
  committed
  68eb692