Provable Contracts

Aprender uses provable contracts — YAML files that define equations, preconditions, postconditions, and falsification tests for every kernel and CLI command.

405 Contracts

ls contracts/*.yaml | wc -l
# 405

Contract Structure

metadata:
  version: 1.0.0
  description: Softmax numerical stability
  references:
  - "Goodfellow et al., Deep Learning, MIT Press 2016"

equations:
  softmax_stability:
    formula: |
      softmax(x) = exp(x - max(x)) / sum(exp(x - max(x)))
    invariants:
    - "output sums to 1.0 (within f32 epsilon)"
    - "max-subtraction prevents overflow"

falsification_tests:
- id: FALSIFY-SOFTMAX-001
  prediction: softmax([1000, 1000, 1000]) does not overflow
  test: cargo test softmax_large_values

Enforcement

Contracts are enforced at three levels:

  1. Compile time: #[contract] proc macro from aprender-contracts-macros
  2. Test time: FALSIFY-* tests verify predictions
  3. CI time: pv lint contracts/ checks schema validity

CLI Contract

Every apr subcommand has a contract entry in contracts/apr-cli-commands-v1.yaml:

apr mono audit  # Runs all contract checks

See: Contract spec