An Elixir-native proof/spec kernel inspired by Lean's trusted-kernel design.

Theoria's public DSL will remain untrusted: macros and tactics may generate proof terms, but only Theoria.Kernel can admit checked constants and definitions into an environment.