diff --git a/Dockerfile b/Dockerfile
index 5e1b7649..474a4928 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -6,7 +6,7 @@ ARG TARGETARCH
 ARG GOARCH
 
 # See https://github.com/initia-labs/movevm/releases
-ENV LIBMOVEVM_VERSION=v0.4.2
+ENV LIBMOVEVM_VERSION=v0.4.3
 
 # Install necessary packages
 RUN set -eux; apk add --no-cache ca-certificates build-base git cmake
diff --git a/cmd/move/move.go b/cmd/move/move.go
index f8f0e50b..6b6e142a 100644
--- a/cmd/move/move.go
+++ b/cmd/move/move.go
@@ -19,11 +19,9 @@ import (
 	movetypes "github.com/initia-labs/initia/x/move/types"
 
 	"github.com/initia-labs/movevm/api"
-	"github.com/initia-labs/movevm/types/compiler"
+	"github.com/initia-labs/movevm/types"
 	buildtypes "github.com/initia-labs/movevm/types/compiler/build"
-	coveragetypes "github.com/initia-labs/movevm/types/compiler/coverage"
 	docgentypes "github.com/initia-labs/movevm/types/compiler/docgen"
-	provetypes "github.com/initia-labs/movevm/types/compiler/prove"
 	testtypes "github.com/initia-labs/movevm/types/compiler/test"
 	"github.com/pelletier/go-toml"
 	"github.com/spf13/cobra"
@@ -51,6 +49,7 @@ const (
 	flagBytecodeVersion        = "bytecode-version"
 	flagCompilerVersion        = "compiler-version"
 	flagLanguageVersion        = "language-version"
+	flagNamedAddresses         = "named-addresses"
 	/* test options */
 	flagGasLimit                  = "gas-limit"
 	flagGasLimitShorthand         = "g"
@@ -66,20 +65,6 @@ const (
 	flagComputeCoverage           = "coverage"
 	// clean options
 	flagCleanCache = "clean-cache"
-	// prove options
-	flagProcCores           = "proc-cores"
-	flagTrace               = "trace"
-	flagTraceShorthand      = "t"
-	flagCVC5                = "cvc5"
-	flagStratificationDepth = "stratification-depth"
-	flagRandomSeed          = "random-seed"
-	flagVcTimeout           = "vc-timeout"
-	flagCheckInconsistency  = "check-inconsistency"
-	flagKeepLoops           = "keep-loops"
-	flagLoopUnroll          = "loop-unroll"
-	flagStableTestOutput    = "stable-test-output"
-	flagDump                = "dump"
-	flagVerbosity           = "verbosity"
 	// verify options
 	flagVerify = "verify"
 	// coverage options
@@ -116,7 +101,6 @@ func MoveCommand(ac address.Codec) *cobra.Command {
 		moveNewCmd(),
 		moveCleanCmd(),
 		moveDeployCmd(ac),
-		moveProveCmd(),
 		moveVerifyCmd(),
 		moveDocgenCmd(),
 	)
@@ -178,7 +162,7 @@ func moveTestCmd() *cobra.Command {
 			if err != nil {
 				return err
 			}
-			tc, err := getTestConfig(cmd)
+			tc, err := getTestOptions(cmd)
 			if err != nil {
 				return err
 			}
@@ -249,7 +233,7 @@ func moveCoverageSummaryCmd() *cobra.Command {
 				return err
 			}
 
-			config, err := getCoverageSummaryConfig(cmd)
+			config, err := getCoverageSummaryOptions(cmd)
 			if err != nil {
 				return err
 			}
@@ -280,8 +264,8 @@ func moveCoverageSourceCmd() *cobra.Command {
 				return err
 			}
 
-			_, err = api.CoverageSource(*arg, coveragetypes.CoverageSourceConfig{
-				ModuleName: args[0],
+			_, err = api.CoverageSource(*arg, types.CompilerCoverageSourceOptions{
+				ModuleName: &args[0],
 			})
 			if err != nil {
 				return err
@@ -307,8 +291,8 @@ func moveCoverageBytecodeCmd() *cobra.Command {
 				return err
 			}
 
-			_, err = api.CoverageBytecode(*arg, coveragetypes.CoverageBytecodeConfig{
-				ModuleName: args[0],
+			_, err = api.CoverageBytecode(*arg, types.CompilerCoverageBytecodeOptions{
+				ModuleName: &args[0],
 			})
 			if err != nil {
 				return err
@@ -355,7 +339,7 @@ func moveCleanCmd() *cobra.Command {
 		Long:  "Remove previously built data and its cache",
 		Args:  cobra.ExactArgs(0),
 		RunE: func(cmd *cobra.Command, args []string) error {
-			arg := compiler.CompilerArgument{}
+			arg := types.CompilerArguments{}
 
 			cleanCache, err := cmd.Flags().GetBool(flagCleanCache)
 			if err != nil {
@@ -509,38 +493,6 @@ func moveDeployCmd(ac address.Codec) *cobra.Command {
 	return cmd
 }
 
-func moveProveCmd() *cobra.Command {
-	cmd := &cobra.Command{
-		Use:   "prove [flags]",
-		Short: "prove a move package",
-		Long:  "run formal verification of a Move package using the Move prover",
-		Args:  cobra.ExactArgs(0),
-		RunE: func(cmd *cobra.Command, args []string) error {
-			arg, err := getCompilerArgument(cmd)
-			if err != nil {
-				return err
-			}
-
-			pc, err := getProveConfig(cmd)
-			if err != nil {
-				return err
-			}
-
-			_, err = api.ProveContract(*arg, *pc)
-			if err != nil {
-				return err
-			}
-
-			fmt.Println("Prove success")
-			return nil
-		},
-	}
-
-	addMoveBuildFlags(cmd)
-	addMoveProveFlags(cmd)
-	return cmd
-}
-
 func moveVerifyCmd() *cobra.Command {
 	cmd := &cobra.Command{
 		Use:   "verify [flags]",
@@ -578,7 +530,7 @@ func moveDocgenCmd() *cobra.Command {
 			if err != nil {
 				return err
 			}
-			dgc, err := getDocgenConfig(cmd)
+			dgc, err := getDocgenOptions(cmd)
 			if err != nil {
 				return err
 			}
@@ -617,6 +569,7 @@ the 'tests' directory`)
 	cmd.Flags().Uint32(flagBytecodeVersion, 0, "Specify the version of the bytecode the compiler is going to emit")
 	cmd.Flags().Uint32(flagCompilerVersion, 1, "Specify the version of the compiler to use")
 	cmd.Flags().Uint32(flagLanguageVersion, 1, "Specify the version of the language to use")
+	cmd.Flags().String(flagNamedAddresses, "", "Named addresses to use in compilation. ex: --named-addresses 'name_1=0x1,name_2=0x2'")
 }
 
 func addMoveTestFlags(cmd *cobra.Command) {
@@ -642,21 +595,6 @@ func addMoveDeployFlags(cmd *cobra.Command) {
 	cmd.Flags().Bool(flagVerify, false, "Verify the contract compared to the onchain package")
 }
 
-func addMoveProveFlags(cmd *cobra.Command) {
-	cmd.Flags().Uint(flagProcCores, provetypes.DefaultProcCores, "The number of cores to use for parallel processing of verification conditions")
-	cmd.Flags().BoolP(flagTrace, flagTraceShorthand, false, "Whether to display additional information in error reports. This may help debugging but also can make verification slower")
-	cmd.Flags().Bool(flagCVC5, false, "Whether to use cvc5 as the smt solver backend. The environment variable `CVC5_EXE` should point to the binary")
-	cmd.Flags().Uint(flagStratificationDepth, provetypes.DefaultStratificationDepth, "The depth until which stratified functions are expanded")
-	cmd.Flags().Uint(flagRandomSeed, 0, "A seed to the prover")
-	cmd.Flags().Uint(flagVcTimeout, provetypes.DefaultVcTimeout, "A (soft) timeout for the solver, per verification condition, in seconds")
-	cmd.Flags().Bool(flagCheckInconsistency, false, "Whether to check consistency of specs by injecting impossible assertions")
-	cmd.Flags().Bool(flagKeepLoops, false, "Whether to keep loops as they are and pass them on to the underlying solver")
-	cmd.Flags().Uint(flagLoopUnroll, 0, "Number of iterations to unroll loops")
-	cmd.Flags().Bool(flagStableTestOutput, false, "Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test output")
-	cmd.Flags().Bool(flagDump, false, "Whether to dump intermediate step results to files")
-	cmd.Flags().StringP(flagVerbosity, flagVerboseShorthand, "", "Verbosity level")
-}
-
 func addMoveDocgenFlags(cmd *cobra.Command) {
 	cmd.Flags().Bool(flagIncludeImpl, false, "Whether to include private declarations and implementations into the generated documentation.")
 	cmd.Flags().Bool(flagIncludeSpecs, false, "Whether to include specifications in the generated documentation.")
@@ -667,7 +605,7 @@ func addMoveDocgenFlags(cmd *cobra.Command) {
 	cmd.Flags().String(flagReferencesFile, "", "Package-relative path to a file whose content is added to each generated markdown file.")
 }
 
-func getCompilerArgument(cmd *cobra.Command) (*compiler.CompilerArgument, error) {
+func getCompilerArgument(cmd *cobra.Command) (*types.CompilerArguments, error) {
 	bc, err := getBuildConfig(cmd)
 	if err != nil {
 		return nil, err
@@ -683,18 +621,18 @@ func getCompilerArgument(cmd *cobra.Command) (*compiler.CompilerArgument, error)
 		return nil, err
 	}
 
-	return &compiler.CompilerArgument{
-		PackagePath: packagePath,
+	return &types.CompilerArguments{
+		PackagePath: &packagePath,
 		Verbose:     verbose,
 		BuildConfig: *bc,
 	}, nil
 }
 
-func getBuildConfig(cmd *cobra.Command) (*buildtypes.BuildConfig, error) {
+func getBuildConfig(cmd *cobra.Command) (*types.CompilerBuildConfig, error) {
 
-	options := []func(*buildtypes.BuildConfig){}
+	options := []func(*types.CompilerBuildConfig){}
 
-	boolFlags := map[string]func(*buildtypes.BuildConfig){}
+	boolFlags := map[string]func(*types.CompilerBuildConfig){}
 	boolFlags[flagDevMode] = buildtypes.WithDevMode()
 	boolFlags[flagTestMode] = buildtypes.WithTestMode()
 	boolFlags[flagGenerateDocs] = buildtypes.WithGenerateDocs()
@@ -736,15 +674,38 @@ func getBuildConfig(cmd *cobra.Command) (*buildtypes.BuildConfig, error) {
 	}
 	options = append(options, buildtypes.WithLanguageVersion(languageVersion))
 
+	namedAddresses, err := cmd.Flags().GetString(flagNamedAddresses)
+	if err != nil {
+		return nil, err
+	}
+	if len(namedAddresses) > 0 {
+		namedAddressMap := make(map[string]types.AccountAddress)
+		for _, namedAddress := range strings.Split(namedAddresses, ",") {
+			v := strings.Split(namedAddress, "=")
+			if len(v) != 2 {
+				return nil, fmt.Errorf("invalid named-addresses: %s", namedAddresses)
+			}
+
+			name := v[0]
+			addr, err := types.NewAccountAddress(v[1]) // validate address
+			if err != nil {
+				return nil, fmt.Errorf("invalid address: %s", v[1])
+			}
+
+			namedAddressMap[name] = addr
+		}
+		options = append(options, buildtypes.WithNamedAddresses(namedAddressMap))
+	}
+
 	bc := buildtypes.NewBuildConfig(options...)
 
 	return &bc, nil
 }
 
-func getTestConfig(cmd *cobra.Command) (*testtypes.TestConfig, error) {
-	options := []func(*testtypes.TestConfig){}
+func getTestOptions(cmd *cobra.Command) (*types.CompilerTestOptions, error) {
+	options := []func(*types.CompilerTestOptions){}
 
-	boolFlags := map[string]func(*testtypes.TestConfig){}
+	boolFlags := map[string]func(*types.CompilerTestOptions){}
 	boolFlags[flagComputeCoverage] = testtypes.WithComputeCoverage()
 	boolFlags[flagReportStatistics] = testtypes.WithReportStatistics()
 	boolFlags[flagReportStorageOnError] = testtypes.WithReportStorageOnError()
@@ -768,11 +729,11 @@ func getTestConfig(cmd *cobra.Command) (*testtypes.TestConfig, error) {
 		options = append(options, testtypes.WithFilter(filter))
 	}
 
-	tc := testtypes.NewTestConfig(options...)
+	tc := testtypes.NewTestOptions(options...)
 	return &tc, nil
 }
 
-func getCoverageSummaryConfig(cmd *cobra.Command) (*coveragetypes.CoverageSummaryConfig, error) {
+func getCoverageSummaryOptions(cmd *cobra.Command) (*types.CompilerCoverageSummaryOptions, error) {
 	functions, err := cmd.Flags().GetBool(flagFunctions)
 	if err != nil {
 		return nil, err
@@ -781,78 +742,16 @@ func getCoverageSummaryConfig(cmd *cobra.Command) (*coveragetypes.CoverageSummar
 	if err != nil {
 		return nil, err
 	}
-	return &coveragetypes.CoverageSummaryConfig{
+	return &types.CompilerCoverageSummaryOptions{
 		Functions: functions,
-		OutputCSV: outputCSV,
+		OutputCsv: outputCSV,
 	}, nil
 }
 
-func getProveConfig(cmd *cobra.Command) (*provetypes.ProveConfig, error) {
-	options := []func(*provetypes.ProveConfig){}
-
-	boolFlags := map[string]func(*provetypes.ProveConfig){}
-	boolFlags[flagTrace] = provetypes.WithTrace()
-	boolFlags[flagCVC5] = provetypes.WithCVC5()
-	boolFlags[flagCheckInconsistency] = provetypes.WithCVC5()
-	boolFlags[flagKeepLoops] = provetypes.WithKeepLoops()
-	boolFlags[flagStableTestOutput] = provetypes.WithStableTestOutput()
-	boolFlags[flagDump] = provetypes.WithDump()
-
-	for fn, opt := range boolFlags {
-		flag, err := cmd.Flags().GetBool(fn)
-		if err != nil {
-			return nil, err
-		}
-		if flag {
-			options = append(options, opt)
-		}
-	}
-
-	procCores, err := cmd.Flags().GetUint(flagProcCores)
-	if err != nil {
-		return nil, err
-	}
-	options = append(options, provetypes.WithProcCores(procCores))
-
-	stratificationDepth, err := cmd.Flags().GetUint(flagStratificationDepth)
-	if err != nil {
-		return nil, err
-	}
-	options = append(options, provetypes.WithStratificationDepth(stratificationDepth))
-
-	randomSeed, err := cmd.Flags().GetUint(flagRandomSeed)
-	if err != nil {
-		return nil, err
-	}
-	options = append(options, provetypes.WithRandomSeed(randomSeed))
-
-	vcTimeout, err := cmd.Flags().GetUint(flagVcTimeout)
-	if err != nil {
-		return nil, err
-	}
-	options = append(options, provetypes.WithVcTimeout(vcTimeout))
-
-	loopUnroll, err := cmd.Flags().GetUint(flagLoopUnroll)
-	if err != nil {
-		return nil, err
-	}
-	options = append(options, provetypes.WithLoopUnroll(loopUnroll))
-
-	verbosity, err := cmd.Flags().GetString(flagVerbosity)
-	if err != nil {
-		return nil, err
-
-	}
-	options = append(options, provetypes.WithVerbosity(verbosity))
-
-	pc := provetypes.NewProveConfig(options...)
-	return &pc, nil
-}
-
-func getDocgenConfig(cmd *cobra.Command) (*docgentypes.DocgenConfig, error) {
-	options := []func(*docgentypes.DocgenConfig){}
+func getDocgenOptions(cmd *cobra.Command) (*types.CompilerDocgenOptions, error) {
+	options := []func(*types.CompilerDocgenOptions){}
 
-	boolFlags := map[string]func(*docgentypes.DocgenConfig){}
+	boolFlags := map[string]func(*types.CompilerDocgenOptions){}
 	boolFlags[flagIncludeImpl] = docgentypes.WithIncludeImpl()
 	boolFlags[flagIncludeSpecs] = docgentypes.WithIncludeSpecs()
 	boolFlags[flagSpecsInlined] = docgentypes.WithSpecsInlined()
@@ -881,6 +780,6 @@ func getDocgenConfig(cmd *cobra.Command) (*docgentypes.DocgenConfig, error) {
 		options = append(options, docgentypes.WithReferencesFile(referencesFile))
 	}
 
-	dgc := docgentypes.NewDocgenConfig(options...)
+	dgc := docgentypes.NewDocgenOptions(options...)
 	return &dgc, nil
 }
diff --git a/go.mod b/go.mod
index 157fed77..701ca2cf 100644
--- a/go.mod
+++ b/go.mod
@@ -40,7 +40,7 @@ require (
 	github.com/hashicorp/go-metrics v0.5.3
 	github.com/initia-labs/OPinit v0.4.2
 	// we also need to update `LIBMOVEVM_VERSION` of Dockerfile#9
-	github.com/initia-labs/movevm v0.4.2
+	github.com/initia-labs/movevm v0.4.3
 	github.com/noble-assets/forwarding/v2 v2.0.0-20240521090705-86712c4c9e43
 	github.com/pelletier/go-toml v1.9.5
 	github.com/pkg/errors v0.9.1
diff --git a/go.sum b/go.sum
index 01e04bdf..dc37f999 100644
--- a/go.sum
+++ b/go.sum
@@ -733,8 +733,8 @@ github.com/initia-labs/OPinit/api v0.4.1 h1:Q8etW92LiwekKZxzDYVFdiHF3uOpEA4nyajy
 github.com/initia-labs/OPinit/api v0.4.1/go.mod h1:Xy/Nt3ubXLQ4zKn0m7RuQOM1sj8TVdlNNyek21TGYR0=
 github.com/initia-labs/cometbft v0.0.0-20240802022359-e0a5ce0336b6 h1:ObKvj9nGiKE+MWZ/LnH3rPcXsnBVVn4c30/iw+fMsd4=
 github.com/initia-labs/cometbft v0.0.0-20240802022359-e0a5ce0336b6/go.mod h1:jHPx9vQpWzPHEAiYI/7EDKaB1NXhK6o3SArrrY8ExKc=
-github.com/initia-labs/movevm v0.4.2 h1:5E4YaLyL7bJfL0mqBnMlu2jB5b3nkOys/RpLzuVkM+Q=
-github.com/initia-labs/movevm v0.4.2/go.mod h1:6MxR4GP5zH3JUc1IMgfqAe1e483mZVS7fshPknZPJ30=
+github.com/initia-labs/movevm v0.4.3 h1:BQmhv5zwakjzWDLoGmLFQAyCAbGQkDds1La4w3cOAJ4=
+github.com/initia-labs/movevm v0.4.3/go.mod h1:6MxR4GP5zH3JUc1IMgfqAe1e483mZVS7fshPknZPJ30=
 github.com/jhump/protoreflect v1.15.3 h1:6SFRuqU45u9hIZPJAoZ8c28T3nK64BNdp9w6jFonzls=
 github.com/jhump/protoreflect v1.15.3/go.mod h1:4ORHmSBmlCW8fh3xHmJMGyul1zNqZK4Elxc8qKP+p1k=
 github.com/jmespath/go-jmespath v0.0.0-20180206201540-c2b33e8439af/go.mod h1:Nht3zPeWKUH0NzdCt2Blrr5ys8VGpn0CEB0cQHVjt7k=