There has been a lot of progress in high-assurance cryptographic software. Our aim is to extend this to high-assurance smart contracts. One example of this effort is the Hax toolchain. By embedding the smart contracts, we get clean Rust code. By using Hax we allow software engineers to write security properties and guarantees about the smart contract into the code, which can be translated into ConCert, where it can be verified.