Current limits

The model is bounded, single-threaded C. Unsupported unions, assembly, nonlocal control flow, uncertain identity, type reinterpretation, unavailable call effects and exhausted limits fail selected checking. General recursive heap invariants and arbitrary loop induction are not implemented. Complex pointer-containing paths, callbacks and dynamic expressions require complete facts from their existing models; otherwise the result stays unresolved. Unproved pointer relationships and floating-to-integer conversions remain incomplete. Traversal reasoning is bounded to 64 active variables, 32 loop iterations/candidates and 4,096 relation steps per operation. Exhaustion is reported and supplies no proof. Conservative rejection of valid C is expected.

Library proof models cover allocation/release, bounded memory operations, positive-size realloc, strlen, strnlen, strcpy, stpcpy, strcat, strdup, strndup and strncpy, including supported compiler/fortified spellings. Unknown string lengths or unproved arithmetic can still prevent checking a modeled call. An entry in the broader ordinary ownership table does not by itself establish a complete safety contract. Keep unmodeled dependencies outside selected scope or mark an intentional trust boundary explicitly.

checking-incomplete identifies missing proof; checking-failed identifies a violation. Lowering their diagnostic severity does not discharge the underlying obligation. The compiler still fails selected checking.

The authoritative design and acceptance criteria are in RFC 0018 and RFC 0019, extended by RFC 0021 and RFC 0022.