CertAlloc–An O(1) memory allocator formally verified -TLA+ and CBMC

- CertAlloc is an open-source memory allocator — low-level software that manages how programs request and free memory. Its key claim: guaranteed **O(1)** time and **O(1)** memory overhead for every operation, meaning performance never degrades regardless of usage patterns. - It uses **formal verification** (TLA+ and CBMC) to mathematically prove correctness, not just testing. This is rare for memory allocators. - **TLA+** is a formal specification language by Turing Award winner Leslie Lamport; **CBMC** is a model checker that exhaustively checks C code for bugs. - Most general-purpose allocators (like glibc's malloc) use heuristics with unpredictable performance. CertAlloc targets real-time systems, embedded devices, and safety-critical software where predictable behavior is essential. - Created by a pseudonymous developer, aimed at the embedded/real-time OS community.