diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs
index fc5f5e745..984a585a1 100644
--- a/app/Commands/Format.hs
+++ b/app/Commands/Format.hs
@@ -4,10 +4,9 @@ import Commands.Base
 import Commands.Format.Options
 import Data.Text qualified as Text
 import Juvix.Formatter
-import Juvix.Prelude.Pretty
 
 data FormatNoEditRenderMode
-  = ReformattedFile (NonEmpty AnsiText)
+  = ReformattedFile Text
   | InputPath (Path Abs File)
   | Silent
 
@@ -72,9 +71,9 @@ renderModeFromOptions target opts formattedInfo
   | opts ^. formatInPlace = whenContentsModified (EditInPlace formattedInfo)
   | opts ^. formatCheck = NoEdit Silent
   | otherwise = case target of
-      TargetFile {} -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContentsAnsi))
+      TargetFile {} -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContents))
       TargetProject {} -> whenContentsModified (NoEdit (InputPath (formattedInfo ^. formattedFileInfoPath)))
-      TargetStdin -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContentsAnsi))
+      TargetStdin -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContents))
   where
     whenContentsModified :: FormatRenderMode -> FormatRenderMode
     whenContentsModified res
@@ -91,9 +90,9 @@ renderFormattedOutput target opts fInfo = do
       EditInPlace i@FormattedFileInfo {..} ->
         runTempFileIO
           . restoreFileOnError _formattedFileInfoPath
-          $ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText)
+          $ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContents)
       NoEdit m -> case m of
-        ReformattedFile ts -> forM_ ts renderStdOut
+        ReformattedFile ts -> renderStdOut ts
         InputPath p -> say (pack (toFilePath p))
         Silent -> return ()
 
diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs
index bf993bef1..a1a9b2d74 100644
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@@ -36,6 +36,7 @@ import Juvix.Compiler.Pipeline.Package.Loader.EvalEff.IO
 import Juvix.Compiler.Pipeline.Repl
 import Juvix.Compiler.Pipeline.Run
 import Juvix.Compiler.Pipeline.Setup (entrySetup)
+import Juvix.Data.CodeAnn (Ann)
 import Juvix.Data.Effect.Git
 import Juvix.Data.Effect.Process
 import Juvix.Data.Error.GenericError qualified as Error
@@ -308,9 +309,9 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
             printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
             printDoc = \case
               Nothing -> do
-                s' <- ppConcrete s
-                renderOut (mkAnsiText @Text "No documentation available for ")
-                renderOutLn s'
+                let s' :: Doc Ann = pretty s
+                    msg = "No documentation available for" <+> s'
+                renderOutLn (toAnsiText True msg)
               Just ju -> printConcrete ju
 
             getDocFunction :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
diff --git a/src/Juvix/Compiler/Concrete/Print.hs b/src/Juvix/Compiler/Concrete/Print.hs
index 8e9ce8f56..a29a2ea0c 100644
--- a/src/Juvix/Compiler/Concrete/Print.hs
+++ b/src/Juvix/Compiler/Concrete/Print.hs
@@ -15,7 +15,7 @@ ppOutDefaultNoComments :: (PrettyPrint c) => c -> AnsiText
 ppOutDefaultNoComments = mkAnsiText . PPOutput . docNoComments defaultOptions
 
 ppOutDefault :: (HasLoc c, PrettyPrint c) => Comments -> c -> AnsiText
-ppOutDefault cs = mkAnsiText . PPOutput . doc defaultOptions cs
+ppOutDefault cs = mkAnsiText . PPOutput . docDefault cs
 
 ppOut :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> Comments -> c -> AnsiText
 ppOut o cs = mkAnsiText . PPOutput . doc (project o) cs
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 5618091eb..057829765 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -70,6 +70,9 @@ doc opts cs x = docHelper (Just (fileComments file cs)) opts x
     file :: Path Abs File
     file = getLoc x ^. intervalFile
 
+docDefault :: (PrettyPrint c, HasLoc c) => Comments -> c -> Doc Ann
+docDefault cs = doc defaultOptions cs
+
 ppModulePathType ::
   forall t s r.
   (SingI t, SingI s, Members '[ExactPrint, Reader Options] r) =>
diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs
index 176609d13..dadef922b 100644
--- a/src/Juvix/Formatter.hs
+++ b/src/Juvix/Formatter.hs
@@ -1,19 +1,18 @@
 module Juvix.Formatter where
 
 import Data.List.NonEmpty qualified as NonEmpty
-import Data.Text qualified as T
 import Juvix.Compiler.Concrete.Language
-import Juvix.Compiler.Concrete.Print (ppOutDefault)
+import Juvix.Compiler.Concrete.Print (docDefault)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
 import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Data.CodeAnn
 import Juvix.Extra.Paths
 import Juvix.Prelude
-import Juvix.Prelude.Pretty
 
 data FormattedFileInfo = FormattedFileInfo
   { _formattedFileInfoPath :: Path Abs File,
-    _formattedFileInfoContentsAnsi :: NonEmpty AnsiText,
+    _formattedFileInfoContents :: Text,
     _formattedFileInfoContentsModified :: Bool
   }
 
@@ -40,18 +39,6 @@ instance Semigroup FormatResult where
 instance Monoid FormatResult where
   mempty = FormatResultOK
 
-combineResults :: [FormatResult] -> FormatResult
-combineResults = mconcat
-
-ansiPlainText :: NonEmpty AnsiText -> Text
-ansiPlainText = T.concat . toList . fmap toPlainText
-
-formattedFileInfoContentsText :: SimpleGetter FormattedFileInfo Text
-formattedFileInfoContentsText = to infoToPlainText
-  where
-    infoToPlainText :: FormattedFileInfo -> Text
-    infoToPlainText fInfo = ansiPlainText (fInfo ^. formattedFileInfoContentsAnsi)
-
 -- | Format a single Juvix file.
 --
 -- If the file requires formatting then the function returns 'FormatResultNotFormatted'.
@@ -68,7 +55,7 @@ format ::
 format p = do
   originalContents <- readFile' p
   runReader originalContents $ do
-    formattedContents <- formatPath p
+    formattedContents :: Text <- formatPath p
     formatResultFromContents formattedContents p
 
 -- | Format a Juvix project.
@@ -102,13 +89,16 @@ formatProject p = do
       Sem r (FormatResult, Recurse Rel)
     handler cd _ files res = do
       let juvixFiles = [cd <//> f | f <- files, isJuvixFile f]
-      subRes <- combineResults <$> mapM format juvixFiles
+      subRes <- mconcat <$> mapM format juvixFiles
       return (res <> subRes, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml && not (isHiddenDirectory d)))
 
-formatPath :: (Members '[Reader Text, ScopeEff] r) => Path Abs File -> Sem r (NonEmpty AnsiText)
+formatPath ::
+  (Members '[Reader Text, ScopeEff] r) =>
+  Path Abs File ->
+  Sem r Text
 formatPath p = do
   res <- scopeFile p
-  formatScoperResult res
+  formatScoperResult False res
 
 formatStdin ::
   forall r.
@@ -118,19 +108,19 @@ formatStdin = do
   res <- scopeStdin
   let originalContents = fromMaybe "" (res ^. Scoper.resultParserResult . resultEntry . entryPointStdin)
   runReader originalContents $ do
-    formattedContents <- formatScoperResult res
+    formattedContents :: Text <- formatScoperResult False res
     formatResultFromContents formattedContents formatStdinPath
 
 formatResultFromContents ::
   forall r.
   (Members '[Reader Text, Output FormattedFileInfo] r) =>
-  NonEmpty AnsiText ->
+  Text ->
   Path Abs File ->
   Sem r FormatResult
 formatResultFromContents formattedContents filepath = do
   originalContents <- ask
   if
-      | originalContents /= ansiPlainText formattedContents -> mkResult FormatResultNotFormatted
+      | originalContents /= formattedContents -> mkResult FormatResultNotFormatted
       | otherwise -> mkResult FormatResultOK
   where
     mkResult :: FormatResult -> Sem r FormatResult
@@ -138,31 +128,42 @@ formatResultFromContents formattedContents filepath = do
       output
         ( FormattedFileInfo
             { _formattedFileInfoPath = filepath,
-              _formattedFileInfoContentsAnsi = formattedContents,
+              _formattedFileInfoContents = formattedContents,
               _formattedFileInfoContentsModified = res == FormatResultNotFormatted
             }
         )
       return res
 
-formatScoperResult :: (Members '[Reader Text] r) => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
-formatScoperResult res = do
+formatScoperResult' ::
+  Bool -> Text -> Scoper.ScoperResult -> Text
+formatScoperResult' force original sres =
+  run . runReader original $ formatScoperResult force sres
+
+formatScoperResult ::
+  (Members '[Reader Text] r) =>
+  Bool ->
+  Scoper.ScoperResult ->
+  Sem r Text
+formatScoperResult force res = do
   let cs = res ^. Scoper.comments
   formattedModules <-
     runReader cs
       . mapM formatTopModule
-      $ res ^. Scoper.resultModules
+      $ res
+        ^. Scoper.resultModules
+  let txt :: Text = toPlainTextTrim . mconcat . NonEmpty.toList $ formattedModules
+
   case res ^. Scoper.mainModule . modulePragmas of
     Just pragmas ->
       case pragmas ^. withLocParam . withSourceValue . pragmasFormat of
         Just PragmaFormat {..}
-          | not _pragmaFormat ->
-              NonEmpty.singleton . mkAnsiText @Text <$> ask
+          | not _pragmaFormat && not force -> ask @Text
         _ ->
-          return formattedModules
+          return txt
     Nothing ->
-      return formattedModules
+      return txt
   where
-    formatTopModule :: (Members '[Reader Comments] r) => Module 'Scoped 'ModuleTop -> Sem r AnsiText
+    formatTopModule :: (Members '[Reader Comments] r) => Module 'Scoped 'ModuleTop -> Sem r (Doc Ann)
     formatTopModule m = do
-      cs <- ask
-      return (ppOutDefault cs m)
+      cs :: Comments <- ask
+      return $ docDefault cs m
diff --git a/src/Juvix/Prelude/Pretty.hs b/src/Juvix/Prelude/Pretty.hs
index 28e44e16d..781bc7646 100644
--- a/src/Juvix/Prelude/Pretty.hs
+++ b/src/Juvix/Prelude/Pretty.hs
@@ -123,6 +123,14 @@ toAnsiText useColors
 toPlainText :: (HasTextBackend a) => a -> Text
 toPlainText = Text.renderStrict . toTextStream
 
+toPlainTextTrim :: (HasTextBackend a) => a -> Text
+toPlainTextTrim =
+  Text.unlines
+    . map Text.stripEnd
+    . dropWhile Text.null
+    . Text.lines
+    . toPlainText
+
 prettyText :: (Pretty a) => a -> Text
 prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
 
@@ -157,31 +165,31 @@ hsepMaybe l
   | null l = Nothing
   | otherwise = Just (hsep l)
 
-nest' :: Doc ann -> Doc ann
+nest' :: Doc a -> Doc a
 nest' = nest 2
 
-indent' :: Doc ann -> Doc ann
+indent' :: Doc a -> Doc a
 indent' = indent 2
 
-hang' :: Doc ann -> Doc ann
+hang' :: Doc a -> Doc a
 hang' = hang 2
 
-spaceOrEmpty :: Doc ann
+spaceOrEmpty :: Doc a
 spaceOrEmpty = flatAlt (pretty ' ') mempty
 
-oneLineOrNext :: Doc ann -> Doc ann
+oneLineOrNext :: Doc a -> Doc a
 oneLineOrNext x = PP.group (flatAlt (line <> indent' x) (space <> x))
 
-oneLineOrNextNoIndent :: Doc ann -> Doc ann
+oneLineOrNextNoIndent :: Doc a -> Doc a
 oneLineOrNextNoIndent x = PP.group (flatAlt (line <> x) (space <> x))
 
-oneLineOrNextBlock :: Doc ann -> Doc ann
+oneLineOrNextBlock :: Doc a -> Doc a
 oneLineOrNextBlock x = PP.group (flatAlt (line <> indent' x <> line) (space <> x <> space))
 
-oneLineOrNextBraces :: Doc ann -> Doc ann
+oneLineOrNextBraces :: Doc a -> Doc a
 oneLineOrNextBraces x = PP.group (flatAlt (lbrace <> line <> indent' x <> line <> rbrace) (lbrace <> x <> rbrace))
 
-nextLine :: Doc ann -> Doc ann
+nextLine :: Doc a -> Doc a
 nextLine x = PP.group (line <> x)
 
 ordinal :: Int -> Doc a
@@ -212,5 +220,5 @@ articleFor n
   | isVowel (Text.head n) = "an"
   | otherwise = "a"
 
-itemize :: (Functor f, Foldable f) => f (Doc ann) -> Doc ann
+itemize :: (Functor f, Foldable f) => f (Doc a) -> Doc a
 itemize = vsep . fmap ("• " <>)
diff --git a/test/Format.hs b/test/Format.hs
index 33a45f851..c70e91b31 100644
--- a/test/Format.hs
+++ b/test/Format.hs
@@ -2,16 +2,17 @@ module Format where
 
 import Base
 import Juvix.Compiler.Concrete qualified as Concrete
-import Juvix.Compiler.Concrete.Print qualified as P
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
 import Juvix.Compiler.Pipeline.Setup
-import Juvix.Prelude.Pretty
+import Juvix.Formatter
 
 data PosTest = PosTest
   { _name :: String,
     _dir :: Path Abs Dir,
-    _file :: Path Abs File
+    _file :: Path Abs File,
+    _expectedFile :: Maybe (Path Abs File),
+    _force :: Bool
   }
 
 makeLenses ''PosTest
@@ -19,13 +20,11 @@ makeLenses ''PosTest
 root :: Path Abs Dir
 root = relToProject $(mkRelDir "tests/positive")
 
-renderCode :: (HasLoc a, P.PrettyPrint a) => P.Comments -> a -> Text
-renderCode c = toPlainText . P.ppOutDefault c
-
-posTest :: String -> Path Rel Dir -> Path Rel File -> PosTest
-posTest _name rdir rfile =
+posTest :: String -> Path Rel Dir -> Path Rel File -> Maybe (Path Rel File) -> Bool -> PosTest
+posTest _name rdir rfile efile _force =
   let _dir = root <//> rdir
       _file = _dir <//> rfile
+      _expectedFile = (_dir <//>) <$> efile
    in PosTest {..}
 
 testDescr :: PosTest -> TestDescr
@@ -37,7 +36,9 @@ testDescr PosTest {..} =
         entryPoint <- defaultEntryPointCwdIO _file
         let maybeFile = entryPoint ^? entryPointModulePaths . _head
         f <- fromMaybeM (assertFailure "Not a module") (return maybeFile)
+
         original :: Text <- readFile (toFilePath f)
+
         step "Parsing"
         p :: Parser.ParserResult <- snd <$> runIO' entryPoint upToParsing
 
@@ -51,11 +52,15 @@ testDescr PosTest {..} =
                   Concrete.fromParsed p
               )
 
-        let formatted :: Text
-            formatted = renderCode (s ^. Scoper.comments) (s ^. Scoper.mainModule)
-
-        step "Format"
-        assertEqDiffText "check: pretty . scope . parse = id" original formatted
+        let formatted = formatScoperResult' _force original s
+        case _expectedFile of
+          Nothing -> do
+            step "Format"
+            assertEqDiffText "check: pretty . scope . parse = id" original formatted
+          Just eFile -> do
+            step "Checking against expected output file"
+            expFile :: Text <- readFile (toFilePath eFile)
+            assertEqDiffText "Compare to expected output" formatted expFile
     }
 
 allTests :: TestTree
@@ -69,9 +74,13 @@ tests =
   [ posTest
       "Format"
       $(mkRelDir ".")
-      $(mkRelFile "Format.juvix"),
-    posTest
-      "Records"
-      $(mkRelDir ".")
       $(mkRelFile "Format.juvix")
+      Nothing
+      False,
+    posTest
+      "TrailingWhitespace"
+      $(mkRelDir ".")
+      $(mkRelFile "LocalModWithAxiom.juvix")
+      (Just $(mkRelFile "LocalModWithAxiom.juvix.formatted"))
+      True
   ]
diff --git a/tests/negative/DefaultArgCycle.juvix b/tests/negative/DefaultArgCycle.juvix
index 9419a3c24..8cec864ca 100644
--- a/tests/negative/DefaultArgCycle.juvix
+++ b/tests/negative/DefaultArgCycle.juvix
@@ -2,5 +2,6 @@ module DefaultArgCycle;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := fun {c := 3} + a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := fun {c := 3}
+  + a
+  + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
diff --git a/tests/negative/Internal/AmbiguousCoercions.juvix b/tests/negative/Internal/AmbiguousCoercions.juvix
index 3eb03893f..d76e38255 100644
--- a/tests/negative/Internal/AmbiguousCoercions.juvix
+++ b/tests/negative/Internal/AmbiguousCoercions.juvix
@@ -3,28 +3,30 @@ module AmbiguousCoercions;
 type Unit := unit;
 
 trait
-type T A := mkT { pp : A → A };
+type T A := mkT {pp : A → A};
 
 trait
-type T1 A := mkT1 { pp : A → A };
+type T1 A := mkT1 {pp : A → A};
 
 trait
-type T2 A := mkT2 { pp : A → A };
+type T2 A := mkT2 {pp : A → A};
 
 instance
-unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
+unitT1 : T1 Unit := mkT1 (pp := λ {_ := unit});
 
 instance
-unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
+unitT2 : T2 Unit := mkT2 (pp := λ {_ := unit});
 
 coercion instance
-fromT1toT {A} {{T1 A}} : T A := mkT@{
-  pp := T1.pp
-};
+fromT1toT {A} {{T1 A}} : T A :=
+  mkT@{
+    pp := T1.pp
+  };
 
 coercion instance
-fromT2toT {A} {{T2 A}} : T A := mkT@{
-  pp := T2.pp
-};
+fromT2toT {A} {{T2 A}} : T A :=
+  mkT@{
+    pp := T2.pp
+  };
 
 main : Unit := T.pp unit;
diff --git a/tests/negative/Internal/CoercionTargetNotATrait.juvix b/tests/negative/Internal/CoercionTargetNotATrait.juvix
index fd8bd0c76..64d9abc6b 100644
--- a/tests/negative/Internal/CoercionTargetNotATrait.juvix
+++ b/tests/negative/Internal/CoercionTargetNotATrait.juvix
@@ -3,7 +3,9 @@ module CoercionTargetNotATrait;
 trait
 type T A := mkT {a : A};
 
-type Maybe A := just A | nothing;
+type Maybe A :=
+  | just A
+  | nothing;
 
 coercion instance
 inst {A} {{T A}} : Maybe A := nothing;
diff --git a/tests/negative/Internal/DefaultArgCycleArity.juvix b/tests/negative/Internal/DefaultArgCycleArity.juvix
index 2e237cc5f..08d56b505 100644
--- a/tests/negative/Internal/DefaultArgCycleArity.juvix
+++ b/tests/negative/Internal/DefaultArgCycleArity.juvix
@@ -2,5 +2,6 @@ module DefaultArgCycleArity;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b
+  + a
+  + 1} : Nat := a * b + c;
diff --git a/tests/negative/Internal/DefaultTypeError.juvix b/tests/negative/Internal/DefaultTypeError.juvix
index 45ee37eb8..4197a6052 100644
--- a/tests/negative/Internal/DefaultTypeError.juvix
+++ b/tests/negative/Internal/DefaultTypeError.juvix
@@ -1,6 +1,7 @@
 module DefaultTypeError;
 
 type T := mkT;
+
 type U := mkU;
 
 g {a : T := mkU} : T := a;
diff --git a/tests/negative/Internal/LoopingCoercion.juvix b/tests/negative/Internal/LoopingCoercion.juvix
index 48decf4a4..97c4b15b1 100644
--- a/tests/negative/Internal/LoopingCoercion.juvix
+++ b/tests/negative/Internal/LoopingCoercion.juvix
@@ -9,13 +9,15 @@ trait
 type T2 A := mkT2 {pp : A -> A};
 
 coercion instance
-fromT1toT2 {A} {{T1 A}} : T2 A := mkT2@{
-  pp := T1.pp
-};
+fromT1toT2 {A} {{T1 A}} : T2 A :=
+  mkT2@{
+    pp := T1.pp
+  };
 
 coercion instance
-fromT2toT1 {A} {{T2 A}} : T1 A := mkT1@{
-  pp := T2.pp
-};
+fromT2toT1 {A} {{T2 A}} : T1 A :=
+  mkT1@{
+    pp := T2.pp
+  };
 
 main : Unit := T1.pp unit;
diff --git a/tests/negative/Termination/Data/Nat.juvix b/tests/negative/Termination/Data/Nat.juvix
index e8c1c1deb..90721c266 100644
--- a/tests/negative/Termination/Data/Nat.juvix
+++ b/tests/negative/Termination/Data/Nat.juvix
@@ -23,11 +23,11 @@ import Data.Bool;
 open Data.Bool;
 
 even : ℕ → Bool
-  
+
   | zero := true
   | (suc n) := odd n;
 
 odd : ℕ → Bool
-  
+
   | zero := false
   | (suc n) := even n;
diff --git a/tests/negative/Termination/DefaultArguments.juvix b/tests/negative/Termination/DefaultArguments.juvix
index caf088074..b146b0277 100644
--- a/tests/negative/Termination/DefaultArguments.juvix
+++ b/tests/negative/Termination/DefaultArguments.juvix
@@ -3,6 +3,7 @@ module DefaultArguments;
 type T := t;
 
 g : T := f;
+
 f {a : T := g} : T := a;
 
 main : T := f;
diff --git a/tests/negative/Termination/Mutual.juvix b/tests/negative/Termination/Mutual.juvix
index d896ac7f5..8b8a8f89e 100644
--- a/tests/negative/Termination/Mutual.juvix
+++ b/tests/negative/Termination/Mutual.juvix
@@ -3,7 +3,7 @@ module Mutual;
 axiom A : Type;
 
 f : A -> A -> A
-  
+
   | x y := g x (f x x);
 
 g : A -> A -> A
diff --git a/tests/negative/Termination/Ord.juvix b/tests/negative/Termination/Ord.juvix
index 2c94f4c59..228bdf9a9 100644
--- a/tests/negative/Termination/Ord.juvix
+++ b/tests/negative/Termination/Ord.juvix
@@ -9,11 +9,11 @@ type Ord :=
   | Lim : (ℕ -> Ord) -> Ord;
 
 addord : Ord -> Ord -> Ord
-  
+
   | Zord y := y
   | (SOrd x) y := SOrd (addord x y)
   | (Lim f) y := Lim (aux-addord f y);
 
 aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
-  
+
   | f y z := addord (f z) y;
diff --git a/tests/negative/Termination/TerminatingF.juvix b/tests/negative/Termination/TerminatingF.juvix
index 1464b97ad..e8e46691f 100644
--- a/tests/negative/Termination/TerminatingF.juvix
+++ b/tests/negative/Termination/TerminatingF.juvix
@@ -4,7 +4,7 @@ axiom A : Type;
 
 terminating
 f : A -> A -> A
-  
+
   | x y := g x (f x x);
 
 g : A -> A -> A
diff --git a/tests/negative/Termination/TerminatingG.juvix b/tests/negative/Termination/TerminatingG.juvix
index ce6eb42c9..7a9a9e426 100644
--- a/tests/negative/Termination/TerminatingG.juvix
+++ b/tests/negative/Termination/TerminatingG.juvix
@@ -3,7 +3,7 @@ module TerminatingG;
 axiom A : Type;
 
 f : A -> A -> A
-  
+
   | x y := g x (f x x);
 
 terminating
diff --git a/tests/positive/DefaultValues.juvix b/tests/positive/DefaultValues.juvix
index 6abbb13c4..b2b1e90c8 100644
--- a/tests/positive/DefaultValues.juvix
+++ b/tests/positive/DefaultValues.juvix
@@ -18,13 +18,13 @@ axiom c : C;
 
 axiom d : D;
 
-mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) : A × f2 × C :=
-  f1, x, f3;
+mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2)
+  : A × f2 × C := f1, x, f3;
 
 x1 : A × B × C := mk (x := b);
 
-mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2) : A × f2 × C :=
-  f1, x, f3;
+mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2)
+  : A × f2 × C := f1, x, f3;
 
 x2 : A × B × C := mk2 (x := b) (y := b);
 
diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix
index fdd58e002..4b8250033 100644
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@@ -188,12 +188,14 @@ f : Nat -> Nat :=
   };
 
 module Patterns;
+
   syntax operator × functor;
   syntax operator , pair;
   type × (A : Type) (B : Type) := , : A → B → A × B;
 
   f : Nat × Nat × Nat × Nat -> Nat
     | (a, b, c, d) := a;
+
 end;
 
 module UnicodeStrings;
@@ -201,6 +203,7 @@ module UnicodeStrings;
 end;
 
 module Comments;
+
   axiom a1 : Type;
   -- attached to a1
 
diff --git a/tests/positive/Internal/Mutual.juvix b/tests/positive/Internal/Mutual.juvix
index f7fdd4cec..6106bed48 100644
--- a/tests/positive/Internal/Mutual.juvix
+++ b/tests/positive/Internal/Mutual.juvix
@@ -13,11 +13,11 @@ not : _
   | true := false;
 
 odd : _
-  
+
   | zero := false
   | (suc n) := even n;
 
 even : _
-  
+
   | zero := true
   | (suc n) := odd n;
diff --git a/tests/positive/LocalModWithAxiom.juvix b/tests/positive/LocalModWithAxiom.juvix
new file mode 100644
index 000000000..3cebbc851
--- /dev/null
+++ b/tests/positive/LocalModWithAxiom.juvix
@@ -0,0 +1,29 @@
+{-# format: false #-}
+module LocalModWithAxiom;                
+
+module A;                    
+          
+  axiom B : Type;           
+         
+end;         
+      
+module C;
+
+
+  
+  axiom D : Type;
+   
+  module E;
+
+
+    
+    axiom F : Type;  
+   
+  end;  
+  
+end;
+   
+
+
+
+   
\ No newline at end of file
diff --git a/tests/positive/LocalModWithAxiom.juvix.formatted b/tests/positive/LocalModWithAxiom.juvix.formatted
new file mode 100644
index 000000000..bc7170d27
--- /dev/null
+++ b/tests/positive/LocalModWithAxiom.juvix.formatted
@@ -0,0 +1,21 @@
+{-# format: false #-}
+module LocalModWithAxiom;
+
+module A;
+
+  axiom B : Type;
+
+end;
+
+module C;
+
+  axiom D : Type;
+
+  module E;
+
+    axiom F : Type;
+
+  end;
+
+end;
+
diff --git a/tests/positive/MutualType.juvix b/tests/positive/MutualType.juvix
index ea9c478f3..1eba04b46 100644
--- a/tests/positive/MutualType.juvix
+++ b/tests/positive/MutualType.juvix
@@ -11,7 +11,7 @@ type List (a : Type) :=
     :: : a → List a → List a;
 
 Forest : Type -> Type
-  
+
   | A := List (Tree A);
 
 --- N-Ary tree.
diff --git a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
index cb12feb00..075e67f1b 100644
--- a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
@@ -4,4 +4,5 @@ import Stdlib.Prelude open;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage {name := "package-juvix"; dependencies := []};
+  defaultPackage
+    {name := "package-juvix"; dependencies := []};
diff --git a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
index ab6b44162..52746ee05 100644
--- a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
@@ -5,6 +5,6 @@ import PackageDescription.V1 open;
 
 package : Package :=
   defaultPackage
-     {name := "abc";
-      version := mkVersion 0 0 0 ;
-      dependencies := [git "name" "url" "ref1"]};
+    {name := "abc";
+     version := mkVersion 0 0 0;
+     dependencies := [git "name" "url" "ref1"]};
diff --git a/tests/positive/Termination/Data/Nat.juvix b/tests/positive/Termination/Data/Nat.juvix
index 08a180dbb..7952e2dc0 100644
--- a/tests/positive/Termination/Data/Nat.juvix
+++ b/tests/positive/Termination/Data/Nat.juvix
@@ -23,11 +23,11 @@ import Data.Bool;
 open Data.Bool;
 
 even : ℕ → Bool
-  
+
   | zero := true
   | (suc n) := odd n;
 
 odd : ℕ → Bool
-  
+
   | zero := false
   | (suc n) := even n;
diff --git a/tests/positive/Termination/Mutual.juvix b/tests/positive/Termination/Mutual.juvix
index f5cc25631..0e04eaa28 100644
--- a/tests/positive/Termination/Mutual.juvix
+++ b/tests/positive/Termination/Mutual.juvix
@@ -4,7 +4,7 @@ axiom A : Type;
 
 terminating
 f : A -> A -> A
-  
+
   | x y := g x (f x x);
 
 terminating
diff --git a/tests/smoke/Commands/format.smoke.yaml b/tests/smoke/Commands/format.smoke.yaml
index 67970624d..7ce374211 100644
--- a/tests/smoke/Commands/format.smoke.yaml
+++ b/tests/smoke/Commands/format.smoke.yaml
@@ -328,3 +328,4 @@ tests:
     stdout:
       contains: juvix format error
     exit-status: 1
+