Se trata de estudiar el diseño y la verificación formal de dos programas moleculares en el modelo débil de Amos que resuelven (a) el problema de la generación de permutaciones; y (b) el problema del camino hamiltoniano en su versión dirigida y sin nodos distinguidos.