Kasmer

K powered property verification for WASM

Kasmer is a tool that utilizes a rigorous formal semantics to provides property testing and verification for the Multivers blockchain. Users can write Rust tests to check if a property is true, such as verifying if the liquidity product remains constant for an automated market maker (AMM) during swaps. These tests utilize random inputs and mathematically verify the validity of the property. With Kasmer, it is not necessary for a user to have specialized verification training or learn new languages to perform this verification.

Why use Kasmer?

Runtime Verification engineers and auditors aim to create a tool that helps developers gain confidence in their code. While developers can write unit tests, they may want to go beyond that. By writing property tests, they can verify specific properties of their code on random input values. With Kasmer, developers can ensure that these properties hold true for all input values.

How Does it Work?

To test a contract A, developers need to write another contract TestA in Rust. TestA should include an endpoint for each property that needs to be tested. Initially, Kasmer runs these endpoints with random inputs, similar to normal property testing. Once the initial tests pass, Kasmer is run again to mathematically prove that the property tests hold true for any input.

Documentation will be provided here as soon as it is available.