Embedded proofs for veri able neural networks