proofs

Not the keyword you're looking for? See all keywords.

Can I prove Concrete programs in Lean? Can I prove Concrete programs in Lean?
10 min read Keywords:  concrete, lean, formal verification, systems programming, proofs

The original roadmap for proving Concrete programs in Lean, updated now that part of that bridge exists: source contracts, proof obligations, Lean-checked evidence, stale detection, and an explicit trusted base.