1. Writing a binary analysis tool is an enormous task. Before getting to the useful and new part, you need a lot of infrastructure (e.g., a scalable intermediate representation). Rolling your own infrastructure is not a great idea IMO, there are great compiler frameworks (LLVM, but GCC would work too) that provide you with a lot of tools to start with. We can literally run the LLVM -O2 optimization pipeline on our IR.
2. In binary analysis there's a trend to use SMT solvers. We absolutely do not, by design. They simply do not scale. Binary analysis theory is really just compiler theory. Have you ever seen a mainstream compiler use SMT solvers for the standard compilation pipeline? No, it does not scale. Depending on what you need to do, you go the old fashioned way and write a data-flow analysis that does what you need, instead of using an SMT solver that can solve much more complex problems but does not scale. At rev.ng, we're in love with Monotone Frameworks. If your analysis fits in the framework, it will run in linear time. It's more difficult than going "Z3 solve it for me", but it scales great. Suggested reading: https://link.springer.com/book/10.1007/978-3-662-03811-6
Don't get me wrong, there are use cases where using an SMT solver makes sense, for instance looking for bugs, but SMT solvers should be a last resource measure for tasks where you're OK with saying "OK, I didn't find anything in 10 minutes, let's bail out". But that's not the case for simply lifting and even decompiling a binary.
This said, I haven't been following closely the developments of rizin, but my comments are more on the general trend in binary analysis that I see.