Aries Design Automation LLC extends the state-of-the-art in technologies for formal verification of hardware and software, cyber security, Boolean Satisfiability (SAT), solving of Constraint Satisfaction Problems (CSPs), planning, and scheduling. In several R&D projects for NASA, The firm is developing technology formally to verify the computer systems on the Crew Exploration Vehicle (CEV), the next generation of spacecraft that will replace the shuttle and will be used for human flights to the Moon, including for building of human bases there.