SPARKNaCl is a new, verified and fast reefrence implementation of the NaCl API, based on the TweetNaCl distribution. It has a fully automated, complete and sound proof of type-safety and several key correctness properties. In addition, the code is fast - out-performing TweetNaCl on an Ed25519 Sign operation by a factor of 3 at all optimization levels. This talk will cover how "Proof Driven Optimization" can result in code that is both correct and fast on bare-metal embedded targets. TweetNaCl is a compact reference implementation of the NaCl API. It was initially constructed to show that an entire crypto library could fit into "100 tweets", but has since been re-used in some critical applications, such as the WireGuard VPN. There are no comments in the code at all, and all assurance rests on a single brief academic paper, and the formidable reputation of the authors. Can we do better? Can we produce a reference implementation which is amenable to automatic verification and yet is competitive with TweetNaCl in terms of performance and code size? This talk presents SPARKNaCl - a complete re-implementation of TweetNaCl in SPARK, which comes with a fully automated proof of type-safety, memory-safety and a number of key correctness properties. Having established a solid foundation, we went on to compare the performance and code size of SPARKNaCl against the original C implementation. Various transformations and optimizations have been applied that result in SPARKNaCl out-performing TweetNaCl on a bare-metal 32-bit RISC-V machine for a single Ed25519 "Sign" operation, while retaining automation and completeness of the proof. Furthermore, SPARKNaCl is freely available under the 3-clause BSD licence. This talk will present an overview of the results from both the proof work and performance analysis of SPARKNaCl.