Yes,even more complicated but no proof that all.

Reference counting enable automated releasing memory if no cycles. Users who use smartpointers in C++ or Swift language must be carefully and proper use weak pointers.
I think about extend smartpointers to manage cycles and start new language which can use this algorithm.
I don’t know if algorithm is correct for all possible graphs and graph forest (set) and all possible adding, removing edges in runtime.
Preview this algorithm
Block must have:

• standard ref count (use count)
• weak count
• outgoing count
• link_number
  In other hand pointers have standard with unlike fat(double) smartpointers in C++.
  For further info, current version biggest method
  https://github.com/parstools/smart/blob/86ca62e9bc6c4dc2e5a2de2408594bedb430140e/testCpp/dyncycles.cpp#L53

main is https://github.com/parstools/smart/blob/86ca62e9bc6c4dc2e5a2de2408594bedb430140e/testCpp/main.cpp#L287

Is possible proof correctness this algorithm or find leaks?

Problem is with directed graph, because is possible many vertex links to one. It is reverse tree. This means,that is impossible leaving spanning tree. Question is another: how detect cycles and remove all cycles?

All algorithms for MST I meet, uses indirect graph and search minimum weight. I need a bit other: my graph is directed, weights are unimportant, all are = 1. Is not necessary find minimal tree, but ANY tree without cycles, although tree with minimal number of edges will be nice. Most important is - graph must be directed.