A matching of a graph is any set of edges in which no two edges share a vertex. Steffens gave a necessary and sufficient condition for countable graphs to have a perfect matching (i.e., a matching that covers all vertices). We analyze the strength of Steffens’ theorem from the viewpoint of computability theory and reverse mathematics. By first restricting to certain kinds of graphs (e.g., graphs with bounded degree and locally finite graphs), we classify some weaker versions of Steffens’ theorem. We then analyze Steffens’ corollary on the existence of maximal matchings, which is critical to his proof of the main theorem. Finally, using methods of Aharoni, Magidor, and Shore, we give a partial result that helps hone in on the computational strength of Steffens’ theorem. Joint with Stephen Flood, Matthew Jura, and Oscar Levin.