Pinned Loading

1. proving-sqlite proving-sqlite Public

   AI agents writing machine-checked CBMC proofs that SQLite's record decoding has no undefined behavior, without changing a byte of SQLite. 18 of 22 functions proved; 2 SQLite bugs and several verifi…

   C

2. lean1090 lean1090 Public

   Formally verified Mode S / ADS-B decoding in Lean 4, with reproducible proofs and benchmarks.

   Lean 1

3. igp24-axplorer igp24-axplorer Public

   Axplorer-based research scaffold for IGP24 polynomial candidate generation

   Python

4. cuboctahedron cuboctahedron Public

   Lean 4 / mathlib formalization (in progress): no nonsingular periodic billiard path in the cuboctahedron bounces off each face exactly once. Exact arithmetic, kernel-checked certificates.

   Lean 1

5. aerostore aerostore Public

   Shared-memory transactional database engine in Rust with partial formal verification

   Rust