aion_verify 3.0.0

A two-tier proof engine, pure Rust: tier 4 checks a predicate against EVERY input in a bounded domain (exhaustive); tier 5 proves properties over UNBOUNDED, multi-variable domains (all of u64) via interval abstract interpretation, including function CONTRACTS (precond -> postcond) — Proven / Refuted-with-witness / honest Unknown, never a false result. no_std, no unsafe, no external solver. A first-party alternative to symbolic model checkers like Kani.
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 }}