Make an existing proof easier to inspect by exposing its hierarchy, dependencies, scope, and unresolved obligations.
Claude Code plugin for formal agent contracts — define inter-agent contracts in VDM-SL, verify with VDMJ, prove with Z3, and auto-generate contract tests for spec-driven multi-agent development
Scoped authorization for AI-shaped scientific work
systemet is a stratified type theory. The name is system + ET, where ET stands for Equality Theory — because the one primitive relation the whole system keeps at the bottom is equality, and everything else is layered above it as discipline rather than added as new relations.
Event-B toolchain in Lean 4 with parsing, checking, proof obligations, and refinement semantics
To associate your repository with the proof-obligations topic, visit your repo's landing page and select "manage topics."