Writing invariants for the compiler & static analyzers


I’m seeking all manner of techniques to create static guarantees, such as typestate and static assertions, to bring the Vulkan API under control. Phantom data and zero-sized type parameters, everything. If it works at compile time to create an invariant, up to the standard lib verification efforts using automated theorem proving, I want to know what it is and start watching repos. Named lifetimes look hard for users, but do seem powerful. What are their use cases and available mechanisms? What else besides const generics is still in flight? What are some tools I can use now to get more coverage and maturity into upstream projects?

I’m Adopting the Vulkan API as a first-class fixer-upper. The API has numerous validation layers to identify invalid call sequences. It also is designed to run in the wild with this validation turned off to go faster. Constraining the API into valid cases is almost completely against its design philosophy, but there are plenty of systems that are basically FSM’s or have at least a dimension that reduces to FSM.