aion_verify 3.8.0

A pure-Rust proof stack with no dependencies and no external solver. Tier 4 exhaustively checks a predicate over a bounded domain; tier 5 proves properties over UNBOUNDED, multi-variable domains via interval abstract interpretation, branch-and-bound refinement, and affine relational reasoning, with function contracts. Also finds faults you never wrote a predicate for -- index-out-of-bounds, overflow, unwrap, division by zero -- by exhaustive execution (std) or symbolically (profile-independent). Plus a tamper-evident SHA-512 hash-chain ledger and post-quantum (hash-based WOTS/Merkle) signatures. no_std, no unsafe.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

name: CI

on:
  push:
    branches: [master]
  pull_request:

# Every push and every pull request — ours AND Dependabot's — must pass all of these before merge.
permissions:
  contents: read

jobs:
  check:
    name: fmt + clippy + test
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: clippy, rustfmt
      - name: Format
        run: cargo fmt --all --check
      - name: Clippy (deny all warnings)
        run: cargo clippy --all-targets -- -D warnings
      - name: Test
        run: cargo test --all-targets

  audit:
    name: security audit
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: rustsec/audit-check@v2
        with:
          token: ${{ secrets.GITHUB_TOKEN }}