| Category | Total | Done | In Progress | Blocked | Remaining |
|---|---|---|---|---|---|
ABI/FFI (ABI) |
5 |
0 |
0 |
0 |
5 |
Typing (TP) |
2 |
0 |
0 |
0 |
2 |
Invariant (INV) |
0 |
0 |
0 |
0 |
0 |
Security (SEC) |
0 |
0 |
0 |
0 |
0 |
Concurrency (CONC) |
0 |
0 |
0 |
0 |
0 |
Algorithm (ALG) |
0 |
0 |
0 |
0 |
0 |
Domain (DOM) |
0 |
0 |
0 |
0 |
0 |
Total |
7 |
0 |
0 |
0 |
7 |
Overall: 0% proven
| ID | Proof | Category | Prover | Priority | Est. Effort |
|---|---|---|---|---|---|
ABI-1 |
Non-null pointer proofs |
ABI |
Idris2 |
P1 |
2h |
ABI-2 |
Memory layout correctness |
ABI |
Idris2 |
P1 |
4h |
ABI-3 |
Platform type size proofs |
ABI |
Idris2 |
P1 |
2h |
ABI-4 |
FFI function return type proofs |
ABI |
Idris2 |
P1 |
2h |
ABI-5 |
C ABI compliance |
ABI |
Idris2 |
P1 |
4h |
TP-1 |
Core data type well-formedness |
TP |
Idris2 |
P1 |
4h |
TP-2 |
Public API type safety |
TP |
Lean4 |
P2 |
4h |
# Check all Idris2 proofs
just proof-check-idris2
# Check all Lean4 proofs
just proof-check-lean4
# Check all Agda proofs
just proof-check-agda
# Check all Coq proofs
just proof-check-coq
# Run all proof checks
just proof-check-all
# Scan for dangerous patterns
panic-attack assail --proofs-only