After learning a thing or two by implementing large-scale blockchain systems for capital markets (e.g. with the DTCC and its member banks), Axoni is making available a new programming language that enables formal verification and heightened security for smart contracts on Ethereum compatable networks. The technology could help prevent hacks that have plagued the crypto universe for years.
Formal verification is a rigorous mathematical method used to prove the correctness of computer programs. Historically, this methodology has been used to fortify software and hardware logic in military systems, transportation infrastructure, cryptography and microprocessors. More recently there is increased awareness of the benefits of formal verification for smart contract code. When designing AxLang, our goal was to maximize security while enabling broad adoption as much as possible. With most programming languages, substantial trade-offs need to be made between those priorities. For example, languages like Haskell or OCaml are known for their powerful functional programming capabilities, but their adoption tends to be limited to relatively small (albeit decidedly passionate) communities.