Is a paraconsistent and provably non-trivial foundation for math possible?

One should note that as regards your question 1, systems of relevant arithmetic with inconsistent models such as $R{\sharp}$, $R{\sharp}{\sharp}$, and the systems $RM3^{i}$ can prove (with finitary proofs) their own non-triviality (see Friedman's and Meyer's paper "Whither Relevant Arithmetic",The Journal of Symbolic Logic, Vol. 57, No. 3(Sep., 1992), pp. 824-831; and Meyer's and Mortensen's paper, "Inconsistent Models for Relevant Arithmetics", Journal of Symbolic Logic, Vol. 49, No. 3 (Sep.,1984)). Note also that (for example) that $PRA$+ $Quantifier-free$ $Transfinite$ $Induction$ $up$ $to$ $\epsilon_0$ can prove the consistency of $PA$, but are incomparable in logical strength. Why then is it necessary that the nontrivial paraconsistent system that can serve as a foundation for mathematics have its non-triviality proven in a weaker formal system?

If one drops the criterion mentioned in question 1 (the proof of non-triviality of a paraconsistent system in a weaker formal system), there is a paraconsistent system in which one can develop standard set theory (and in so doing produces a paraconsistent foundation for mathematics). This is the system Hyper-Frege ($HF$)+ 'There is an infinite well-founded set' ($HF_{\infty}$). $HF$ first appears in Thierry Libert's paper "$ZF$ and the Axiom of Choice in Some Paraconsistent Set Theories" (Logic and Logical Philosophy, Vol. 11 (2003), 91-114; and $HF_{\infty}$ appears in Olivier Esser's paper "A Strong Model of Paraconsistent Logic", Notre Dame Journal of Formal Logic, Vol 44, No. 3 (2003), pp. 149-156. If one considers Esser's Theorem 3.2 (my comments will be in square brackets),

The theory $HF_{\infty}$ is mutually interpretable with $GPK^{+}_{\infty}$ which is also [equiconsistent with] $KM$ [Kelly-Morse class theory] + 'On is weakly compact'. The theory $HF$ is mutually interpretable with $PA_2$ [second-order arithmetic--practitioners of Reverse Mathematics please take note].

one sees that $HF_{\infty}$ can serve as a foundation for most (if not all) modern mathematics, and that most ordinary mathematics can be interpreted and developed in $HF$. It also should be noted that Esser's construction of a model for $HF_{\infty}$ shows that $HF_{\infty}$ is non-trivial. It is unknown to me whether $HF$ or $HF_{\infty}$ can prove their own non-triviality.

There's basically no reason to think that ZFC is inconsistent. Even if it is inconsistent, there's an attractive fragment called Peano arithmetic, which seems self-evidently consistent to me. Gödel's incompleteness still holds here, and it holds in even weaker fragments of arithmetic. It's because as soon as you have a fragment of arithmetic large enough to do anything interesting, you can encode proofs as numbers in that arithmetic, and then you can derive Gödel's results. This seems intrinsic to the nature of arithmetic to me -- proofs are strings of symbols that we can store in a computer, so of course we can represent it as a big number.

That said, people have attempted things in the direction you suggest. One approach is what's called relevance logic. There's a version of arithmetic for relevance logic that is provably non-trivial. My impression is that it only captures a small fragment of arithmetic, though. My link provides additional details, including references for relevance arithmetic.

Zach Weber has been working on developing a paraconsistent set theory that can serve as a foundation for mathematics.