aion_verify 0.3.0

A two-tier proof engine: tier 4 checks a predicate against EVERY input in a bounded domain (exhaustive, not sampling); tier 5 proves properties over UNBOUNDED domains (all of u64) symbolically via interval abstract interpretation — Proven / Refuted-with-witness / honest Unknown, never a false result. Pure Rust, 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@v4
      - 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@v4
      - uses: rustsec/audit-check@v2
        with:
          token: ${{ secrets.GITHUB_TOKEN }}