diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -45,10 +45,11 @@
   , mux
   -- ** Lookups
   , linear
-  -- * Hierarchical Scope
-  , scope
   -- * Statements
   , Stmt
+  -- ** Hierarchical Scope and Annotations
+  , scope
+  , annotate
   -- ** Variable Declarations
   , bool
   , bool'
@@ -215,14 +216,30 @@
 
 -- | Creates a hierarchical scope.
 scope :: Name -> Stmt a -> Stmt a
-scope name (Stmt f0) = Stmt f1
-  where
-  f1 (path, statement) = (a, (path, statement1))
-    where
-    (a, (_, statement1)) = f0 (path ++ [name], statement)
+scope name stmt = do
+  (path0, stmt0) <- get
+  put (path0 ++ [name], stmt0)
+  a <- stmt
+  (_, stmt1) <- get
+  put (path0, stmt1)
+  return a
+
+-- | Add an annotation to a statement.  Useful for requirement trace tags.
+annotate :: Name -> Stmt a -> Stmt a
+annotate name stmt = do
+  (path0, stmt0) <- get
+  put (path0, Null)
+  a <- stmt
+  (_, stmt1) <- get
+  put (path0, stmt0)
+  statement $ Annotate name stmt1
+  return a
   
 get :: Stmt ([Name], Statement)
 get = Stmt $ \ a -> (a, a)
+
+put :: ([Name], Statement) -> Stmt ()
+put s = Stmt $ \ _ -> ((), s)
 
 getPath :: Stmt [Name]
 getPath = do
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -34,6 +34,7 @@
   Sequence a b -> codeStmt a ++ codeStmt b
   Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
   Assume path a -> "// assume " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"
+  Annotate name a -> "// annotate " ++ name ++ "\n" ++ indent (codeStmt a)
   Null -> ""
 
 codeExpr :: E a -> String
@@ -59,7 +60,7 @@
   group a = "(" ++ intercalate " " a ++ ")"
 
 indent :: String -> String
-indent = unlines . map ("  " ++) . lines
+indent = unlines . map ("    " ++) . lines
 
 indent' :: String -> String
 indent' a = case lines a of
diff --git a/Language/ImProve/Core.hs b/Language/ImProve/Core.hs
--- a/Language/ImProve/Core.hs
+++ b/Language/ImProve/Core.hs
@@ -97,6 +97,7 @@
   | Sequence    Statement Statement
   | Assert      Path (E Bool)
   | Assume      Path (E Bool)
+  | Annotate    Name Statement
   | Null
 
 data Const
@@ -120,6 +121,7 @@
   Sequence a b    -> nub $ stmtVars a ++ stmtVars b
   Assert _ a      -> exprVars a
   Assume _ a      -> exprVars a
+  Annotate _ a    -> stmtVars a
   Null            -> []
 
 -- Information about all of an expressions's variables.
diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs
--- a/Language/ImProve/Verify.hs
+++ b/Language/ImProve/Verify.hs
@@ -26,6 +26,7 @@
                ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]
   Branch path cond a b -> [ Branch path cond a (removeAssertions b) | a <- trimAssertions' a ]
                        ++ [ Branch path cond (removeAssertions a) b | b <- trimAssertions' b ]
+  Annotate name a -> [ Annotate name a | a <- trimAssertions a ]
   a -> [a]
 
 -- | Remove all assertions.
@@ -34,6 +35,7 @@
   Assert _ _ -> Null
   Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)
   Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)
+  Annotate name a -> Annotate name $ removeAssertions a
   a -> a
 
 -- | Paths of all assertions.
@@ -42,6 +44,7 @@
   Assert path _  -> [path]
   Sequence a b   -> assertions a ++ assertions b
   Branch _ _ a b -> assertions a ++ assertions b
+  Annotate _ a   -> assertions a
   _ -> []
 
 -- | Trim all unneeded stuff from a program.
@@ -140,6 +143,12 @@
     evalStmt (AND [enabled, NOT a]) onFalse
     env2 <- get
     put env2 { trace = Branch' (pathName path) b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }
+  Annotate name a -> do
+    env0 <- get
+    put env0 { trace = [] }
+    evalStmt enabled a
+    env1 <- get
+    put env1 { trace = Annotate' name (reverse $ trace env1) : trace env0 }
   where
   assign :: AllE a => V a -> E a -> Y ()
   assign a b = do
@@ -241,12 +250,13 @@
   }
 
 data Trace
-  = Init'   Name Var
-  | Cycle'  Int
-  | Input'  Name Var
-  | Assign' Name Var
-  | Assert' Name Var
-  | Branch' Name Var [Trace] [Trace] 
+  = Init'     Name Var
+  | Cycle'    Int
+  | Input'    Name Var
+  | Assign'   Name Var
+  | Assert'   Name Var
+  | Branch'   Name Var [Trace] [Trace] 
+  | Annotate' Name [Trace]
 
 addVar' :: VarInfo -> Y String
 addVar' v = do
@@ -298,8 +308,8 @@
   f a = case a of
     Init' path var -> case lookup var table of
       Nothing -> ""
-      Just value -> "initialize " ++ path ++ " := " ++ value ++ "\n"
-    Cycle' n -> "cycle " ++ show n ++ "\n"
+      Just value -> "initialize " ++ path ++ " <== " ++ value ++ "\n"
+    Cycle' n -> "\nstep " ++ show n ++ "\n"
     Input' path var -> case lookup var table of
       Nothing -> ""
       Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"
@@ -311,10 +321,11 @@
       Just "false" -> "assertion FAILED: " ++ path ++ "\n"
       _ -> ""
     Branch' path cond onTrue onFalse -> case lookup cond table of
-      Just "true"  -> "branch true: "  ++ path ++ "\n" ++ indent (concatMap f onTrue)
-      Just "false" -> "branch false: " ++ path ++ "\n" ++ indent (concatMap f onFalse)
+      Just "true"  -> "ifelse " ++ path ++ " true\n"  ++ indent (concatMap f onTrue)
+      Just "false" -> "ifelse " ++ path ++ " false\n" ++ indent (concatMap f onFalse)
       _ -> ""
+    Annotate' name traces -> "annotate " ++ name ++ "\n" ++ indent (concatMap f traces)
 
 indent :: String -> String
-indent = unlines . map ("  " ++) . lines
+indent = unlines . map ("    " ++) . lines
 
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.0.4
+version: 0.0.5
 
 category: Language