Gradual Verification
A single program spans the verification spectrum — runtime checks
Refinement Reflection
@logic functions — extending the refinement vocabulary with user-defined predicates.
SMT Routing
Verum's verification layer dispatches each obligation through a
Contracts
Contracts attach preconditions, postconditions, and invariants to
Proofs
When SMT cannot discharge an obligation — because the theory is
Cubical & HoTT
Verum's type system includes a cubical fragment — path types,