Steel is a language for developing and proving concurrent programs
embedded in F$^\star$\xspace, a dependently typed programming language and proof
assistant. Based on SteelCore, a concurrent separation logic (CSL)
formalized in F$^\star$\xspace, our work focuses on exposing the proof rules of
the logic in a form that enables programs and proofs to be
effectively co-developed.

Our main contributions include a new formulation of a Hoare logic
of \emph{quintuples} involving both separation logic and first-order
logic, enabling efficient verification condition (VC) generation and
proof discharge using a combination of tactics and SMT solving. We
relate the VCs produced by our quintuple system to solving a system of
associativity-commutativity (AC) unification constraints and develop
tactics to (partially) solve these constraints using AC-matching
modulo SMT-dischargeable equations.

Our system is fully mechanized and implemented in F$^\star$\xspace. We evaluate
it by developing several verified programs and libraries, including
various sequential and concurrent linked data structures, proof
libraries, and a library for 2-party session types. Our experience
leads us to conclude that our system enables a mixture of automated
and interactive proof, making it productive to build programs
foundationally verified against a highly expressive, state-of-the-art CSL.