/unitb-semantics

Proof of soundness of the Unit-B refinement calculus

Primary LanguageLean

unitb-semantics

Travis: Build Status

Using Lean to

  • formally verify the proof obligations of Literate Unit-B
  • verify implementation rules for Unit-B specifications
  • certify proofs created by Literate Unit-B