Alien design is an important, if neglected, side alley in science fiction writing. This is especially true in military SF.
Any modern military could utterly destroy any army of even WW2 vintage with minimal effort (cf any number of Gulf Wars). Nukes are easiest, but the list extends to fuel-air explosives, stand-off precision-guided weaponry, ground-attack jets, apache helicopters and so on.
The aliens had better not be 50 years ahead of us - or 50 years behind us - or it's no contest!
John Ringo's Posleen are perfect. Somewhat modelled after the Chinese 'human wave' attackers in the Korean War, they have slightly-superior weaponry (galactic tech is available to both sides) and make up in vast numbers what they lack in intelligence. As one character points out: "Each of our soldiers has to kill 100 Posleen to give us any chance of winning. "
With this kind of non-human adversary only intelligence, combat engineering and the clever use of terrain can compensate for massively inferior forces. What a fantastic basis for plot development!
---
I have checked. There are quite a few listings of python-based resolution theorem provers on the net. It's apparently seen as a (hard) computer science exercise at undergraduate level.
But of course, there is no benefit unless you do it yourself.
Please, no jokes about building your own friends! (The intention is to build friends for other people).