You could. It is called an automated theorem prover, with the cheap limited version called constraint based programming. Sadly very unavailable for most program

You could. It is called an automated theorem prover, with the cheap limited version called constraint based programming. Sadly very unavailable for most programming languages. Sometimes writing the proof of why it should be like this is tricky, especially when complexity or performance is involved. (But then the tests are hard too.) Linters are essentially constraint systems for code, but not for the program.