I would like to know what is the "correct" algebraic $K$-theory "with proper support". I suppose that the answer should be found in the condensed world, which is mostly inspired the existence of six functors. See Lectures on Condensed Mathematics, Appendix to Lecture VIII.
$\DeclareMathOperator\Tor{Tor}\DeclareMathOperator\Perf{Perf}\DeclareMathOperator\Spec{Spec}$More precisely, given a map $f\colon R\to S$ of finitely generated rings, we have the functor $f_!\colon D(S_\blacksquare)\to D(R_\blacksquare)$ of "direct image with proper support" which preserves small colimits. Suppose that $f$ is of finite $\Tor$-amplitude, then $f_!$ induces a functor $\Perf(S_\blacksquare)\to\Perf(R_\blacksquare)$ between compact objects in $D(S_\blacksquare)$ and $D(R_\blacksquare)$ respectively. The ordinary $K$-theoretic machinery leads to a map $K(\Perf(S_\blacksquare))\to K(\Perf(R_\blacksquare))$ which looks like some kind of "integral along fibers" of $\Spec S\to\Spec R$ for compactly supported cohomologies. However, this does not seem to be satisfactory, since both sides are discrete.
One way to get a condensed structure might be the following: $\Perf(R_\blacksquare)$ (resp. $\Perf(S_\blacksquare)$) should be a "condensed stable symmetric monoidal $\infty$-category". There might be set-theretic issues, but let's ignore them for a moment. Take the maximal groupoid, we get a map of condensed $E_\infty$-monoids and taking the group completion, we get a map of condensed spectra.
Edit: I was mistaken, we should pass to the Waldhausen $S_\bullet$ construction for this, but seemingly this could also be equipped with a condensed structure.
It is not immediately clear whether these spectra are solid. Is there alternative characterizations of these condensed spectra, hopefully without reference to "condensed $\infty$-categories"?
On the other hand, there is a concept of condensed $K$-theory in Lectures on Analytic Geometry, Prop 10.6. However, this does not seem to coincide with the construction above.
Update: As Denis-Charles Cisinski pointed out, the approach sketched above does not work since the corresponding $K$-theory is trivial by Eilenberg's Swindle applied to the infinite product). It is not immediate for me what is a replacement, in view of the compactly supported topological $K$-theory, for example.