Compiler-enforced evidence levels and a verified coding agent, built on Lean 4
Separate what a Lean module claims from how each claim is established. Five evidence levels (from UnprovenConjecture to ProvenTheorem), compiler-enforced, with a build-time trust report.
ArchitectureA coding agent written in Lean 4 with kernel-verified safety: confined paths, closed tool set, call-graph reachability proofs, and a proven compression budget.
Agent